Theorem: Let $G$ be a finite group, $H\le G$, $F$ a field. Let $U$ be an $F[H]$-module and $V$ an $F[G]$-module; $U^G$ is induced $F[G]$-module. Then, $$U^G\otimes_F V\cong (U\otimes_F V_H)^G \,\,\,\, \mbox{(isomorphic as $F[G]$-modules)}$$
This theorem is mentioned in Jacobson's volume 2 (see $\S 5.10$,Theorem 5.17(3), p. 292-293). But I didn't get clue for the proof by Jacobson. He points out the following in beginning of proof of this theorem: we have two $F[G]$-modules $(F[G]\otimes_{F[H]} U)\otimes_F V$ and $F[G]\otimes_{F[H]} (U\otimes_F V)$, and the natural $F$-vector space isomorphism of these spaces, $(a\otimes x)\otimes y\mapsto a\otimes (x\otimes y)$ is not $F[G]$-module homomorphism. (Then he constructs new $F[G]$-modue isomorphism of them.)
Q. I tried to write alternate proof in following way; I wanted to know, is it correct?
(i) Let $t=[G:H]$ and $G=\cup_{i=1}^t g_iH$ ($g_1=1$). Then W.L.G, we can take $U^G=\oplus_i g_iU$.
(ii) So $U^G\otimes_F V\cong (U\otimes_F V) \oplus \cdots \oplus (g_tU\otimes_F V)$ as $F[G]$-module.
(iii) The decomposition of $F[G]$-module in (ii) satisfies following properties:
$G$ permutes the $t$ many components (subspaces) transitively.
stabilizer of subspace $U\otimes_F V$ is precisely $H$ (so $U\otimes_F V=U\otimes_F V_H$).
So the $F[G]$-module in RHS of $(ii)$ is isomorphic to $(U\otimes_F V_H)^G$ as $F[G]$-module. q.e.d.
Yes, your proof is correct. This characterisation of induction, namely that an $F[G]$-module $W$ having an $F[H]$-submodule $U$ such that $\dim W = [G:H]\dim U$ and $U$ generates $W$ as an $F[G]$-module is very powerful and gives many other elegant proofs.