theorem Th58: :: GROUP_24:58

for G being Group
for H, K being Subgroup of G
for phi being Function of (product <*H,K*>),G st ( for h, k being Element of G st h in H & k in K holds
phi . <*h,k*> = h * k ) holds
( phi is one-to-one iff H /\ K = (1). G )