Modules $(K\otimes A)\otimes_{K}\left(K\otimes B\right)$ and $K\otimes(A\otimes B)$ isomorphic? Let $K$ denote a commutative ring and let $A$ denote an abelian
group.
The tensor product $K\otimes A$ can be looked at as a $K$-module
equipped the action determined by: $$r\cdot s\otimes a=\left(rs\right)\otimes a$$
This module is free over abelian group $A$.
If we also have abelian group $B$ then similarly we can construct
$K$-modules $K\otimes B$ and $K\otimes\left(A\otimes B\right)$.
My question is: 

Are the $K$-modules $\left(K\otimes A\right)\otimes_{K}\left(K\otimes B\right)$
  and $K\otimes\left(A\otimes B\right)$ isomorphic in $\mathbf{Mod}\left(K\right)$, and if so how to prove it?


Own effort:
I suspect there is an isomorphism $\left(K\otimes A\right)\otimes_{K}\left(K\otimes B\right)\to K\otimes\left(A\otimes B\right)$
that is determined by: $$\left(r\otimes a\right)\otimes_{K}\left(s\otimes b\right)\mapsto\left(rs\right)\otimes\left(a\otimes b\right)$$
To prove its existence in $\mathbf{Mod}\left(K\right)$ I
feel forced to prove the existence of a bilinear function: $$f:\left(K\otimes A\right)\times\left(K\otimes B\right)\to K\otimes\left(A\otimes B\right)$$
and that is the place where I got stuck: if I restrict to stating that $f$ is prescribed by $$\left(r\otimes a,s\otimes b\right)\mapsto\left(rs\right)\otimes\left(a\otimes b\right)$$
then it seems to me that I am not ready yet in the sense that it is not shown that $f$ is well defined. This because I have "defined"
$f$ then only on pairs of pure tensors (corresponding bilinear functions are lacking).
 A: One short way of getting the desired isomorphism is
\begin{align*}
  (K \otimes A) \otimes_K (K \otimes B)
  &\cong
  (A \otimes K) \otimes_K (K \otimes B)
  \\
  &\cong
  A \otimes (K \otimes_K (K \otimes B))
  \tag{$\ast$}
  \\
  &\cong
  A \otimes K \otimes B
  \\
  &\cong
  K \otimes A \otimes B
  \\
  &\cong
  K \otimes (A \otimes B)
\end{align*}
where we use for $(\ast)$ the (generalized) associativity over the tensor product.

To explicitely construct the mutually inverse homomorphisms
\begin{align*}
  F
  &\colon
  (K \otimes A) \otimes_K (K \otimes B)
  \to
  K \otimes_K (A \otimes B) \,,
  \\
  G
  &\colon
  K \otimes_K (A \otimes B)
  \to
  (K \otimes A) \otimes_K (K \otimes B)
\end{align*}
we can proceed like you suspect.
To construct the bilinear map
\begin{align*}
  f
  \colon
  (K \otimes A) \times (K \otimes B)
  &\to
  K \otimes (A \otimes B) \,,
  \\
  (\lambda \otimes a, \mu \otimes b)
  &\mapsto
  (\lambda \mu) \otimes (a \otimes b)
\end{align*}
we start with the $\mathbb{Z}$-multilinear map
\begin{align*}
  f''
  \colon
  K \times A \times K \times B
  &\to
  K \otimes (A \otimes B) \,,
  \\
  (\lambda, a, \mu, b)
  &\mapsto
  (\lambda \mu) \otimes (a \otimes b) \,.
\end{align*}
For fixed $(\lambda, a) \in K \times A$ we get a $\mathbb{Z}$-bilinear map
\begin{align*}
  f''_{(\lambda,a)}
  \colon
  K \times B
  &\to
  K \otimes (A \otimes B) \,,
  \\
  (\mu, b)
  &\mapsto
  (\lambda \mu) \otimes (a \otimes b)
\end{align*}
and thus an induced $\mathbb{Z}$-linear map
\begin{align*}
  f'_{(\lambda,a)}
  \colon
  K \otimes B
  &\to
  K \otimes (A \otimes B) \,,
  \\
  \mu \otimes b
  &\mapsto
  (\lambda \mu) \otimes (a \otimes b) \,.
\end{align*}
The mapping $(\lambda,a) \mapsto f''_{(\lambda,a)}$ is itself $\mathbb{Z}$-bilinear by the $\mathbb{Z}$-multilinearity of $f''$, whence the mapping $(\lambda,a) \mapsto f'_{(\lambda,a)}$ is $\mathbb{Z}$-linear.
The resulting map
\begin{align*}
  f'
  \colon
  K \times A \times (K \otimes B)
  &\to
  K \otimes (A \otimes B) \,,
  \\
  (\lambda, a, \mu \otimes b)
  &\mapsto
  f'_{(\lambda,a)}(\mu \otimes b)
  =
  (\lambda \mu) \otimes (a \otimes b) \,.
\end{align*}
is therefore $\mathbb{Z}$-trilinear.
For fixed $t \in K \otimes B$ we now get again a $\mathbb{Z}$-bilinear map
\begin{align*}
  f'_{t}
  \colon
  K \times A
  &\to
  K \otimes (A \otimes B) \,,
  \\
  (\lambda, a)
  &\mapsto
  f'(\lambda, a, t) \,.
\end{align*}
that results again in a $\mathbb{Z}$-linear map
\begin{align*}
  f_t
  \colon
  K \otimes A
  &\to
  K \otimes (A \otimes B) \,,
  \\
  \lambda \otimes a
  &\mapsto
  f'(\lambda, a, t) \,.
\end{align*}
It follows from the $\mathbb{Z}$-trilinearity of $f'$ that the mapping $t \mapsto f'_t$ is $\mathbb{Z}$-linear, whence the mapping $t \mapsto f_t$ is $\mathbb{Z}$-linear.
This means that the now resulting map
\begin{align*}
  f
  \colon
  (K \otimes A) \times (K \otimes B)
  &\to
  K \otimes (A \otimes B) \,,
  \\
  (s, t)
  &\mapsto
  f_t(u)
\end{align*}
is $\mathbb{Z}$-bilinear.
For $s = \lambda \otimes a$ and $t = \mu \otimes b$ we have by construction
\begin{align*}
  f(\lambda \otimes a, \mu \otimes b)
  &=
  f_{\mu \otimes b}(\lambda \otimes a)
  \\
  &=
  f'(\lambda, a, \mu \otimes b)
  \\
  &=
  f'_{(\lambda, a)}(\mu \otimes b)
  \\
  &=
  f''_{(\lambda, a)}(\mu, b)
  \\
  &=
  (\lambda \mu) \otimes (a \otimes b) \,.
\end{align*}
Now we need to check that the $\mathbb{Z}$-bilinear map $f$ is already $K$-bilinear.
For this we still need that
$$
  f(\kappa \cdot s, t)
  =
  \kappa \cdot f(s,t)
  =
  f(s, \kappa \cdot t)
$$
for all $\kappa \in K$ and $s \in K \otimes A$, $t \in K \otimes B$.
We may assume that $s$,$t$ are simple tensors $s = \lambda \otimes a$ and $t = \mu \otimes b$ and then
\begin{align*}
  f(\kappa \cdot (\lambda \otimes a), (\mu \otimes b))
  &=
  f((\kappa \lambda) \otimes a, \mu \otimes b)
  \\
  &=
  (\kappa \lambda \mu) \otimes (a \otimes b)
  \\
  &=
  \kappa \cdot ((\lambda \mu) \otimes (a \otimes b))
  \\
  &=
  \kappa \cdot f(\lambda \otimes a, \mu \otimes b) \,.
\end{align*}
The other equation can be shown in the same way.
It follows that $f$ induces a $K$-linear map
\begin{align*}
  F
  \colon
  (K \otimes A) \otimes_K (K \otimes B)
  &\to
  K \otimes (A \otimes B) \,,
  \\
  (\lambda \otimes a, \mu \otimes b)
  &\mapsto
  (\lambda \mu) \otimes (a \otimes b) \,.
\end{align*}
To construct the inverse $G$ of $F$ we can play the same game:
We start with a $\mathbb{Z}$-trilinear map
\begin{align*}
  g''
  \colon
  K \times A \times B
  &\to
  (K \otimes A) \otimes_K (K \otimes B) \,,
  \\
  (\lambda, a, b)
  &\mapsto
  (\lambda \otimes a) \otimes (1 \otimes b) \,.
\end{align*}
(Note that it dosen’t matter in which tensor factor $K \otimes A$ or $K \otimes B$ we put $\lambda$.)
Then we get
\begin{align*}
  g'_{\lambda}
  &\colon
  A \times B
  \to
  (K \otimes A) \otimes_K (K \otimes B) \,,
  \\
  g_{\lambda}
  &\colon
  A \otimes B
  \to
  (K \otimes A) \otimes_K (K \otimes B) \,,
  \\
  g
  &\colon
  K \times (A \otimes B)
  \to
  (K \otimes A) \otimes_K (K \otimes B) \,,
  \\
  G
  &\colon
  K \otimes (A \otimes B)
  \to
  (K \otimes A) \otimes_K (K \otimes B) \,,
\end{align*}
It can then be checked on simple tensors that the maps $F$ and $G$ are mutually inverse.

Another way to construct $F$ is by the tensor-$\operatorname{Hom}$-adjunction:
The map
$$
  A \times B
  \to
  A \otimes B \,,
  \quad
  (a,b)
  \mapsto
  ab
$$
is $\mathbb{Z}$-bilinear and hence corresponds a $\mathbb{Z}$-linear map
$$
  A
  \to
  \operatorname{Hom}_{\mathbb{Z}}(B, A \otimes B) \,.
$$
Every homomorphism $B \to A \otimes B$ can be extended to a $K$-linear map $K \otimes B \to K \otimes (A \otimes B)$, giving a $\mathbb{Z}$-linear map
\begin{align*}
  \operatorname{Hom}_{\mathbb{Z}}(B, A \otimes B)
  &\to
  \operatorname{Hom}_K(K \otimes B, K \otimes (A \otimes B)) \,,
  \\
  h
  &\mapsto
  \mathrm{id}_K \otimes h \,.
\end{align*}
By composing the above two $\mathbb{Z}$-linear maps we get a $\mathbb{Z}$-linear map
$$
  A
  \to
  \operatorname{Hom}_K(K \otimes B, K \otimes (A \otimes B)) \,.
$$
The right hand side is a $K$-module, so by extension of scalars we get a $K$-linear map
$$
  K \otimes A
  \to
  \operatorname{Hom}_K(K \otimes B, K \otimes (A \otimes B)) \,.
$$
This $K$-linear map corresponds to a $K$-bilinear map
$$
  (K \otimes A) \times (K \otimes B)
  \to
  K \otimes (A \otimes B) \,,
$$
which is precisely $f$, and hence to a $K$-linear map
$$
  (K \otimes A) \otimes_K (K \otimes B)
  \to
  K \otimes (A \otimes B) \,,
$$
which is precisely $F$.
