for G being finite strict commutative Group
for p being Prime
for m being Nat st card G = p |^ m holds
ex K being strict normal Subgroup of G ex n, k being Nat ex g being Element of G st
( ord g = upper_bound (Ordset G) & K is finite & K is commutative & the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st
( b1 in K & a1 in gr {g} & x = b1 * a1 ) ) & ord g = p |^ n & k = m - n & n <= m & card K = p |^ k & ex F being Homomorphism of (product <*K,(gr {g})*>),G st
( F is bijective & ( for a, b being Element of G st a in K & b in gr {g} holds
F . <*a,b*> = a * b ) ) )