for G being finite commutative Group
for h, k being non zero Nat st card G = h * k & h,k are_coprime holds
ex H, K being finite strict Subgroup of G st
( card H = h & card K = k & the carrier of H /\ the carrier of K = {(1_ G)} & ex F being Homomorphism of (product <*H,K*>),G st
( F is bijective & ( for a, b being Element of G st a in H & b in K holds
F . <*a,b*> = a * b ) ) )