let G be finite strict commutative Group; :: thesis: 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 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 b₃ -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; :: thesis: 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 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 b₂ -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; :: thesis: ( card G = p |^ m implies 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 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 b₁ -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 ; :: thesis: 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 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 b₁ -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 )

proof

let y be Element of G; :: thesis: 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 )
y in the carrier of G ;
then y in rng HFG by P1, FUNCT_2:def 3;
then consider x being object such that
P2: ( x in the carrier of (product F) & y = HFG . x ) by FUNCT_2:11;
reconsider x = x as Seg k -defined total Function by P2, XLM18Th401;
P3: for p being Element of Seg k holds x . p in F . p

proof

let p be Element of Seg k; :: thesis: x . p in F . p
consider R being non empty multMagma such that
P4: ( R = F . p & x . p in the carrier of R ) by XLM18Th402, P2;
thus x . p in F . p by P4; :: thesis: verum

end;

rng x c= the carrier of G

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng x or y in the carrier of G )
assume y in rng x ; :: thesis: y in the carrier of G
then consider i being object such that
D2: ( i in dom x & y = x . i ) by FUNCT_1:def 3;
reconsider i = i as Element of Seg k by D2;
consider R being non empty multMagma such that
P4: ( R = F . i & x . i in the carrier of R ) by P2, XLM18Th402;
reconsider i0 = i as Nat ;
consider ai being Element of G such that
XX2: ( ai = a . i0 & F . i0 = gr {ai} & ord ai = p |^ (Inda . i0) ) by P1;
the carrier of (F . i) c= the carrier of G by XX2, GROUP_2:def 5;
hence y in the carrier of G by D2, P4; :: thesis: verum

end;

then reconsider x = x as Seg k -defined the carrier of G -valued total Function by RELAT_1:def 19;
take x ; :: thesis: ( ( for p being Element of Seg k holds x . p in F . p ) & y = Product x )
thus ( ( for p being Element of Seg k holds x . p in F . p ) & y = Product x ) by P1, P2, P3; :: thesis: verum

end;

now :: thesis: for x1, x2 being Seg k -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 x1, x2 be Seg k -defined the carrier of G -valued total Function; :: thesis: ( ( 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 implies x1 = x2 )
assume AS2: ( ( 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 ) ; :: thesis: x1 = x2
( x1 in product F & HFG . x1 = Product x1 ) by AS2, P1;
then P4: HFG . x1 = HFG . x2 by AS2, P1;
( x1 in the carrier of (product F) & x2 in the carrier of (product F) ) by AS2, P1, STRUCT_0:def 5;
hence x1 = x2 by P4, P1, FUNCT_2:19; :: thesis: verum

end;

hence 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 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 b₁ -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; :: thesis: verum