theorem :: GROUP_18:21

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 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)} ) & ( for y being Element of G ex 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 ) & y = Product x ) ) & ( for x1, x2 being Seg b₄ -defined the carrier of b₁ -valued total Function st ( for p being Element of Seg k holds x1 . p in F . p ) & ( for p being Element of Seg k holds x2 . p in F . p ) & Product x1 = Product x2 holds
x1 = x2 ) )