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_{3} -element FinSequence of G ex Inda being b_{3} -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_{3} -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_{3} -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_{2} -element FinSequence of G ex Inda being b_{2} -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_{2} -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_{2} -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_{1} -element FinSequence of G ex Inda being b_{1} -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_{1} -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_{1} -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_{1} -element FinSequence of G ex Inda being b_{1} -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_{1} -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_{1} -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 )_{1} -element FinSequence of G ex Inda being b_{1} -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_{1} -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_{1} -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

for m being Nat st card G = p |^ m holds

ex k being non zero Nat ex a being b

( ( 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

( ( for p being Element of Seg k holds x . p in F . p ) & y = Product x ) ) & ( for x1, x2 being Seg b

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

( ( 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

( ( for p being Element of Seg k holds x . p in F . p ) & y = Product x ) ) & ( for x1, x2 being Seg b

x1 = x2 ) )

let m be Nat; :: thesis: ( card G = p |^ m implies ex k being non zero Nat ex a being b

( ( 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

( ( for p being Element of Seg k holds x . p in F . p ) & y = Product x ) ) & ( for x1, x2 being Seg b

x1 = x2 ) ) )

assume card G = p |^ m ; :: thesis: ex k being non zero Nat ex a being b

( ( 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

( ( for p being Element of Seg k holds x . p in F . p ) & y = Product x ) ) & ( for x1, x2 being Seg b

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

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;( ( 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

rng x c= the carrier of G
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;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

proof

then reconsider x = x as Seg k -defined the carrier of G -valued total Function by RELAT_1:def 19;
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;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

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

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

hence
ex k being non zero Nat ex a being bx1 = 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;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

( ( 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

( ( for p being Element of Seg k holds x . p in F . p ) & y = Product x ) ) & ( for x1, x2 being Seg b

x1 = x2 ) ) by P1, P4; :: thesis: verum