Equivalence of Internal & External Direct Product (I know that the first part already exists. But I didn't found the second neither here or in books. I also have some further questions.)

Theorem. Let  $G $ be a group.
  
  
*
  
*If  $G$ is the Internal Direct Product of the subgroups  $H,K \leq G $, then  $G $ is isomorphic to the External Direct Product of 
  subgroups $H,K $.
  
*If $G $ is isomorphic to the External Direct Product of  $H,K $ then there exists two normal subgroups $H',K'\leq G$ such that $G$ is
  the Internal Direct Product of $H',K'$.
  

Proof. 1. From the definition, if $G$ is the Internal Direct Product of the subgroups  $H,K \leq G $, then $G=HK$. If we define the function $\xi:H\times K \longrightarrow HK=G, (h,k)\mapsto\xi(h,k):=hk$, we can easily show that is a group isomorphism.


*For this part we will write $H\otimes K$ the internal and $H\times K$ the external direct product. 
So, if $G\cong H\times K $ there is a group isomorphism $\phi: H\times K \longrightarrow G$. We will write $\tilde{H}:=H\times \{1_K \}$, and $\tilde{K}:=\{1_H\}\times K$. We define $H':=\phi(\tilde{H}),\ K':=\phi(\tilde{K})\subseteq G$. Then,


(1) $H'\leq G$, because if $x,y\in H'\iff \exists h_1,h_2 \in H : \phi (h_1,1_K)=x,\ \phi (h_2,1_K)=y \implies xy^{-1}=\phi (h_1,1_K)\phi (h_2,1_K)^{-1}=\phi (h_1h_2^{-1},1_K)\in H'$ and   $H'\trianglelefteq G$ because if $g\in G, n' \in H'\iff \exists n \in H:\phi(n,1_K)=n'$ then $gn'g^{-1}=g\phi({n,1_K})g^{-1}$ but $\phi$ is onto, so for $g \in G,\exists (h,k)\in H\times K:g=\phi(h,k)$. So, $gn'g^{-1}=\phi(h,k)\phi(n,1_K)\phi(h,k)^{-1}=\phi(hnh^{-1},1_K)\in H'$ ($\phi $ is homomorphism). Samely, $K'\trianglelefteq G$.
(2)  $x\in H'\cap K'\iff x\in H'$ and $x\in K' \iff \exists h \in H: \phi(h,1_K)=x$ and $\exists k\in K:\phi(1_H,k)=x \implies \phi(h,1_K)=\phi(1_H,k)\iff h=1_H, k=1_K$ (because $\phi$ is 1-1) $\implies H'\cap K'=\{(1_H,1_K)\}$.
(3) At last, $G=H'K'$ because $\phi$ is onto, and if we take an element $g\in G, \exists (h,k)\in H\times K: \phi(h,k) =g$. So, $g=\phi(h,k)=\phi(h,1_K)\phi(1_H,k)\in H'K'$.
So, $G=H'\otimes K'$.
My questions.
1) Is this proof completely right? 
2) How should we identify these two notions in our minds (for e.g. in free abelian groups)?
Thank you in advance.
 A: 1)
The proof seems correct in essence. I would avoid thing like 'if' and '$\Leftrightarrow$' in the same statement as the logic gets a little ambiguous. This can be a matter of taste, but try to stick to just words or just symbols.
2)
The point of this result is that internal and external direct products are essentially the same thing. An internal direct product may be thought of as a way to split up a given group into two smaller groups and an external direct product may be thought of as a way to construct a group from two smaller groups.
Usually we find it easier to imagine external direct product as we have elements of the form $(x,y)$ where we may treat $x$ and $y$ as elements of two independent groups. However, given a group $G$ it may not be clear that we can split $G$ in this way and the way we do it may not be unique. For example $C_{30}\cong C_5\times C_6\cong C_{10}\times C_3$. These two representations may be thought of as two different, but isomorphic, external products. For direct products, I can't think of any reason why one representation may be better than another, except for group classification (e.g. the classification of finitely generated abelian groups), but for the more general internal / external semidirect product we might choose the external semidirect product that we are most comfortable computing in.
