Is there a theorem stating that disjoint cycles generate distinct elements? If we have a group $H=\langle (12345),(678) \rangle$, it's obvious that $|H|=|(12345)|\cdot |(678)|=15$, because the cycles are disjoint.
Is there some theorem stating this?
 A: You're asking whether $\#\langle H_1, H_2\rangle = \#H_1 \# H_2$ for subgroups $H_1, H_2$ of a group $G$ with $[H_1, H_2] = 1$ (that is, $[h_1, h_2] = 1$ for all $h_i\in H_i$). As you said, that's obvious: the map $H_1\times H_2 \to \langle H_1, H_2\rangle$ given by $(h_1, h_2) \to h_1 h_2$ is a well-defined isomorphism.
A: The direct product of two finite groups $G_1$ and $G_2$ is the group $G_1 \times G_2 :=\{ (g_1,g_2): g_1 \in G_1, g_2 \in G_2\}$, with the group operation defined componentwise, ie $(g_1,g_2)(h_1,h_2):=(g_1 h_1, g_2 h_2)$.  It's clear that the order of $G_1 \times G_2$ is $|G_1|~|G_2|$.  
It can be shown that if $a$ and $b$ are two disjoint permutations, then the permutation group $\langle a, b \rangle $ is isomorphic to the direct product $ \langle a \rangle \times \langle b \rangle$. You can give an isomorphism between these two groups. Or, you can prove that the permutation group $G=\langle a, b \rangle$ is equal to the internet direct product $\langle a \rangle \times \langle b \rangle$ of its subgroups $\langle a \rangle$ and $\langle b \rangle$ by proving that each factor is normal in $G$, the two factors have a trivial intersection, and that $\langle a \rangle \langle b \rangle = G$. 
