for G being finite strict commutative Group
for p being Prime
for m being Nat st card G = p |^ m holds
ex k being non zero Nat ex a being b₄ -element FinSequence of G ex Inda being b₄ -element FinSequence of NAT ex F being Group-like associative commutative multMagma-Family of Seg k ex HFG being Homomorphism of (product F),G st
( ( for i being Nat st i in Seg k holds
ex ai being Element of G st
( ai = a . i & F . i = gr {ai} & ord ai = p |^ (Inda . i) ) ) & ( for i being Nat st 1 <= i & i <= k - 1 holds
Inda . i <= Inda . (i + 1) ) & ( for p, q being Element of Seg k st p <> q holds
the carrier of (F . p) /\ the carrier of (F . q) = {(1_ G)} ) & HFG is bijective & ( for x being Seg b₄ -defined the carrier of b₁ -valued total Function st ( for p being Element of Seg k holds x . p in F . p ) holds
( x in product F & HFG . x = Product x ) ) )