Solution (source code)

= Solution

Assume (I). Existence of a decomposition is part of the hypothesis. If $h_1h_2=k_1k_2$ are two decompositions, multiply on the left by $k_1^{-1}$ and on the right by $h_2^{-1}$ to obtain
$$
k_1^{-1}h_1=k_2h_2^{-1}.
$$
The left side belongs to $H_1$ and the right side to $H_2$, since they are <subgroups>. Their common value belongs to $H_1\cap H_2=\{e\}$, so $h_1=k_1$ and $h_2=k_2$. This proves uniqueness, hence (II).

Conversely, assume (II). Existence immediately gives $G=H_1H_2$. If $a\in H_1\cap H_2$, then
$$
a=a\cdot e=e\cdot a
$$
are two allowed factorizations, because the identity is in each <subgroup>. Uniqueness makes their first components equal, so $a=e$. Thus $H_1\cap H_2=\{e\}$ and (I) follows.

Therefore \b[(I) and (II) are equivalent]. This is an <exact factorization of a group>. For finite <groups> it gives $|G|=|H_1||H_2|$, but it does not by itself identify $G$ with a <direct product of groups>; multiplication between the two factors can be noncommutative.