Product of a subgroup with a normal subgroup ($H\le G,K⊴G⟹HK\le G$)

If $H$ is a subgroup and $K$ a normal subgroup of a group $G$, their product set $HK=\{hk:h\in H,k\in K\}$ is a subgroup. Normality gives $(h_1{k}_1)(h_2{k}_2)=h_1{h}_2(h_2^{-1}{k}_1{h}_2)k_2\in HK$ and $(hk{)}^{-1}=h^{-1}(h{k}^{-1}{h}^{-1})\in HK$. Together with the identity element this proves the subgroup test. For finite subgroups, $|HK|=|H||K|/|H\cap K|$: the pairs representing one product differ exactly by multiplying the first factor by an element of $H\cap K$ and its second factor by its inverse.