for G being finite commutative Group
for h, k being Nat st card G = h * k & h,k are_coprime holds
ex H, K being finite strict Subgroup of G st
( the carrier of H = { x where x is Element of G : x |^ h = 1_ G } & the carrier of K = { x where x is Element of G : x |^ k = 1_ G } & H is normal & K is normal & ( for x being Element of G ex a, b being Element of G st
( a in H & b in K & x = a * b ) ) & the carrier of H /\ the carrier of K = {(1_ G)} )