let G be 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 b3 -element FinSequence of G ex Inda being b3 -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 b3 -defined the carrier of G -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 b3 -defined the carrier of G -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 ) )
let p be Prime; for m being Nat st card G = p |^ m holds
ex k being non zero Nat ex a being b2 -element FinSequence of G ex Inda being b2 -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 b2 -defined the carrier of G -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 b2 -defined the carrier of G -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 ) )
let m be Nat; ( card G = p |^ m implies ex k being non zero Nat ex a being b1 -element FinSequence of G ex Inda being b1 -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 b1 -defined the carrier of G -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 b1 -defined the carrier of G -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 ) ) )
assume
card G = p |^ m
; ex k being non zero Nat ex a being b1 -element FinSequence of G ex Inda being b1 -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 b1 -defined the carrier of G -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 b1 -defined the carrier of G -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 ) )
then consider k being non zero Nat, a being k -element FinSequence of G, Inda being k -element FinSequence of NAT , F being Group-like associative commutative multMagma-Family of Seg k, HFG being Homomorphism of (product F),G such that
P1:
( ( 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 k -defined the carrier of G -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 ) ) )
by LM205A;
set I = Seg k;
P4:
for y being Element of G ex x being Seg k -defined the carrier of G -valued total Function st
( ( for p being Element of Seg k holds x . p in F . p ) & y = Product x )
hence
ex k being non zero Nat ex a being b1 -element FinSequence of G ex Inda being b1 -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 b1 -defined the carrier of G -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 b1 -defined the carrier of G -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 ) )
by P1, P4; verum