defpred S_{1}[ Nat] means for G being finite strict commutative Group

for p being Prime st card G = p |^ $1 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 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 i, j being Element of Seg k st i <> j holds

the carrier of (F . i) /\ the carrier of (F . j) = {(1_ G)} ) & HFG is bijective & ( for x being Seg b_{3} -defined the carrier of b_{1} -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 ) ) );

P1: for n being Nat st ( for k being Nat st k < n holds

S_{1}[k] ) holds

S_{1}[n]
_{1}[k]
from NAT_1:sch 4(P1);

hence 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_{4} -element FinSequence of G ex Inda being b_{4} -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_{4} -defined the carrier of b_{1} -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 ) ) ) ; :: thesis: verum

for p being Prime st card G = p |^ $1 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 i, j being Element of Seg k st i <> j holds

the carrier of (F . i) /\ the carrier of (F . j) = {(1_ G)} ) & HFG is bijective & ( for x being Seg b

( x in product F & HFG . x = Product x ) ) );

P1: for n being Nat st ( for k being Nat st k < n holds

S

S

proof

for k being Nat holds S
let n be Nat; :: thesis: ( ( for k being Nat st k < n holds

S_{1}[k] ) implies S_{1}[n] )

assume APN: for k being Nat st k < n holds

S_{1}[k]
; :: thesis: S_{1}[n]

thus S_{1}[n]
:: thesis: verum

end;S

assume APN: for k being Nat st k < n holds

S

thus S

proof

let G be finite strict commutative Group; :: thesis: for p being Prime st card G = p |^ n 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 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 i, j being Element of Seg k st i <> j holds

the carrier of (F . i) /\ the carrier of (F . j) = {(1_ G)} ) & HFG is bijective & ( for 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 ) holds

( x in product F & HFG . x = Product x ) ) )

let p be Prime; :: thesis: ( card G = p |^ n 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 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 i, j being Element of Seg k st i <> j holds

the carrier of (F . i) /\ the carrier of (F . j) = {(1_ G)} ) & HFG is bijective & ( for 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 ) holds

( x in product F & HFG . x = Product x ) ) ) )

assume AS1: card G = p |^ n ; :: 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 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 i, j being Element of Seg k st i <> j holds

the carrier of (F . i) /\ the carrier of (F . j) = {(1_ G)} ) & HFG is bijective & ( for 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 ) holds

( x in product F & HFG . x = Product x ) ) )

then consider H being strict normal Subgroup of G, n0, m0 being Nat, g0 being Element of G such that

P8: ( ord g0 = upper_bound (Ordset G) & H is finite & H is commutative & the carrier of H /\ the carrier of (gr {g0}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in H & a1 in gr {g0} & x = b1 * a1 ) ) & ord g0 = p |^ n0 & m0 = n - n0 & n0 <= n & card H = p |^ m0 & ex I0 being Homomorphism of (product <*H,(gr {g0})*>),G st

( I0 is bijective & ( for a, b being Element of G st a in H & b in gr {g0} holds

I0 . <*a,b*> = a * b ) ) ) by LM204;

end;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 i, j being Element of Seg k st i <> j holds

the carrier of (F . i) /\ the carrier of (F . j) = {(1_ G)} ) & HFG is bijective & ( for x being Seg b

( x in product F & HFG . x = Product x ) ) )

let p be Prime; :: thesis: ( card G = p |^ n 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 i, j being Element of Seg k st i <> j holds

the carrier of (F . i) /\ the carrier of (F . j) = {(1_ G)} ) & HFG is bijective & ( for x being Seg b

( x in product F & HFG . x = Product x ) ) ) )

assume AS1: card G = p |^ n ; :: 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 i, j being Element of Seg k st i <> j holds

the carrier of (F . i) /\ the carrier of (F . j) = {(1_ G)} ) & HFG is bijective & ( for x being Seg b

( x in product F & HFG . x = Product x ) ) )

then consider H being strict normal Subgroup of G, n0, m0 being Nat, g0 being Element of G such that

P8: ( ord g0 = upper_bound (Ordset G) & H is finite & H is commutative & the carrier of H /\ the carrier of (gr {g0}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in H & a1 in gr {g0} & x = b1 * a1 ) ) & ord g0 = p |^ n0 & m0 = n - n0 & n0 <= n & card H = p |^ m0 & ex I0 being Homomorphism of (product <*H,(gr {g0})*>),G st

( I0 is bijective & ( for a, b being Element of G st a in H & b in gr {g0} holds

I0 . <*a,b*> = a * b ) ) ) by LM204;

per cases
( n = n0 or n <> n0 )
;

end;

suppose BBB:
n = n0
; :: 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 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 i, j being Element of Seg k st i <> j holds

the carrier of (F . i) /\ the carrier of (F . j) = {(1_ G)} ) & HFG is bijective & ( for 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 ) holds

( x in product F & HFG . x = Product x ) ) )

( ( 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 i, j being Element of Seg k st i <> j holds

the carrier of (F . i) /\ the carrier of (F . j) = {(1_ G)} ) & HFG is bijective & ( for x being Seg b

( x in product F & HFG . x = Product x ) ) )

reconsider q = 1 as non zero Nat ;

set K = gr {g0};

set I = {q};

set F = {q} --> G;

card G = card (gr {g0}) by AS1, BBB, P8, GR_CY_1:7;

then X10: G = gr {g0} by GROUP_2:73;

reconsider a = <*g0*> as q -element FinSequence of G by FINSEQ_1:74;

VV1: n0 is Element of NAT by ORDINAL1:def 12;

reconsider Inda = <*n0*> as q -element FinSequence of NAT by VV1, FINSEQ_1:74;

Z1: for i being Nat st i in Seg q holds

ex ai being Element of G st

( ai = a . i & ({q} --> G) . i = gr {ai} & ord ai = p |^ (Inda . i) )

Inda . i <= Inda . (i + 1)

y is non empty multMagma

GG1: for s, t being Element of {q} st s <> t holds

the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)}

AR2: for i being Element of {q} holds F . i is associative ;

for i being Element of {q} holds F . i is commutative ;

then reconsider F = F as Group-like associative commutative multMagma-Family of {q} by AR1, GROUP_7:def 6, AR2, GROUP_7:def 7, GROUP_7:def 8;

F = q .--> G ;

then consider HFG being Homomorphism of (product F),G such that

X4: ( HFG is bijective & ( for x being {q} -defined the carrier of G -valued total Function holds HFG . x = Product x ) ) by GROUP_17:26;

F = q .--> G ;

then for x being {q} -defined the carrier of G -valued total Function st ( for p being Element of {q} holds x . p in F . p ) holds

( x in product F & HFG . x = Product x ) by X4, GROUP_17:25;

hence 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 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 i, j being Element of Seg k st i <> j holds

the carrier of (F . i) /\ the carrier of (F . j) = {(1_ G)} ) & HFG is bijective & ( for 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 ) holds

( x in product F & HFG . x = Product x ) ) ) by X4, GG1, Z1, Z2, FINSEQ_1:2; :: thesis: verum

end;set K = gr {g0};

set I = {q};

set F = {q} --> G;

card G = card (gr {g0}) by AS1, BBB, P8, GR_CY_1:7;

then X10: G = gr {g0} by GROUP_2:73;

reconsider a = <*g0*> as q -element FinSequence of G by FINSEQ_1:74;

VV1: n0 is Element of NAT by ORDINAL1:def 12;

reconsider Inda = <*n0*> as q -element FinSequence of NAT by VV1, FINSEQ_1:74;

Z1: for i being Nat st i in Seg q holds

ex ai being Element of G st

( ai = a . i & ({q} --> G) . i = gr {ai} & ord ai = p |^ (Inda . i) )

proof

Z2:
for i being Nat st 1 <= i & i <= q - 1 holds
let i be Nat; :: thesis: ( i in Seg q implies ex ai being Element of G st

( ai = a . i & ({q} --> G) . i = gr {ai} & ord ai = p |^ (Inda . i) ) )

assume ASD1: i in Seg q ; :: thesis: ex ai being Element of G st

( ai = a . i & ({q} --> G) . i = gr {ai} & ord ai = p |^ (Inda . i) )

D57: i = 1 by TARSKI:def 1, ASD1, FINSEQ_1:2;

then D58: Inda . i = n0 by FINSEQ_1:40;

a . i = g0 by D57, FINSEQ_1:40;

hence ex ai being Element of G st

( ai = a . i & ({q} --> G) . i = gr {ai} & ord ai = p |^ (Inda . i) ) by ASD1, D58, P8, X10, FINSEQ_1:2, FUNCOP_1:7; :: thesis: verum

end;( ai = a . i & ({q} --> G) . i = gr {ai} & ord ai = p |^ (Inda . i) ) )

assume ASD1: i in Seg q ; :: thesis: ex ai being Element of G st

( ai = a . i & ({q} --> G) . i = gr {ai} & ord ai = p |^ (Inda . i) )

D57: i = 1 by TARSKI:def 1, ASD1, FINSEQ_1:2;

then D58: Inda . i = n0 by FINSEQ_1:40;

a . i = g0 by D57, FINSEQ_1:40;

hence ex ai being Element of G st

( ai = a . i & ({q} --> G) . i = gr {ai} & ord ai = p |^ (Inda . i) ) by ASD1, D58, P8, X10, FINSEQ_1:2, FUNCOP_1:7; :: thesis: verum

Inda . i <= Inda . (i + 1)

proof

for y being set st y in rng ({q} --> G) holds
let i be Nat; :: thesis: ( 1 <= i & i <= q - 1 implies Inda . i <= Inda . (i + 1) )

assume ( 1 <= i & i <= q - 1 ) ; :: thesis: Inda . i <= Inda . (i + 1)

then ( 1 <= i & i <= 0 ) ;

hence Inda . i <= Inda . (i + 1) ; :: thesis: verum

end;assume ( 1 <= i & i <= q - 1 ) ; :: thesis: Inda . i <= Inda . (i + 1)

then ( 1 <= i & i <= 0 ) ;

hence Inda . i <= Inda . (i + 1) ; :: thesis: verum

y is non empty multMagma

proof

then reconsider F = {q} --> G as multMagma-Family of {q} by GROUP_7:def 1;
let y be set ; :: thesis: ( y in rng ({q} --> G) implies y is non empty multMagma )

assume y in rng ({q} --> G) ; :: thesis: y is non empty multMagma

then consider x being object such that

D4: ( x in dom ({q} --> G) & y = ({q} --> G) . x ) by FUNCT_1:def 3;

thus y is non empty multMagma by FUNCOP_1:7, D4; :: thesis: verum

end;assume y in rng ({q} --> G) ; :: thesis: y is non empty multMagma

then consider x being object such that

D4: ( x in dom ({q} --> G) & y = ({q} --> G) . x ) by FUNCT_1:def 3;

thus y is non empty multMagma by FUNCOP_1:7, D4; :: thesis: verum

GG1: for s, t being Element of {q} st s <> t holds

the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)}

proof

AR1:
for i being Element of {q} holds F . i is Group-like
;
let s, t be Element of {q}; :: thesis: ( s <> t implies the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)} )

assume GG11: s <> t ; :: thesis: the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)}

s = q by TARSKI:def 1;

hence the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)} by GG11, TARSKI:def 1; :: thesis: verum

end;assume GG11: s <> t ; :: thesis: the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)}

s = q by TARSKI:def 1;

hence the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)} by GG11, TARSKI:def 1; :: thesis: verum

AR2: for i being Element of {q} holds F . i is associative ;

for i being Element of {q} holds F . i is commutative ;

then reconsider F = F as Group-like associative commutative multMagma-Family of {q} by AR1, GROUP_7:def 6, AR2, GROUP_7:def 7, GROUP_7:def 8;

F = q .--> G ;

then consider HFG being Homomorphism of (product F),G such that

X4: ( HFG is bijective & ( for x being {q} -defined the carrier of G -valued total Function holds HFG . x = Product x ) ) by GROUP_17:26;

F = q .--> G ;

then for x being {q} -defined the carrier of G -valued total Function st ( for p being Element of {q} holds x . p in F . p ) holds

( x in product F & HFG . x = Product x ) by X4, GROUP_17:25;

hence 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 i, j being Element of Seg k st i <> j holds

the carrier of (F . i) /\ the carrier of (F . j) = {(1_ G)} ) & HFG is bijective & ( for x being Seg b

( x in product F & HFG . x = Product x ) ) ) by X4, GG1, Z1, Z2, FINSEQ_1:2; :: thesis: verum

suppose AAA:
n <> n0
; :: 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 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 i, j being Element of Seg k st i <> j holds

the carrier of (F . i) /\ the carrier of (F . j) = {(1_ G)} ) & HFG is bijective & ( for 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 ) holds

( x in product F & HFG . x = Product x ) ) )

( ( 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 i, j being Element of Seg k st i <> j holds

the carrier of (F . i) /\ the carrier of (F . j) = {(1_ G)} ) & HFG is bijective & ( for x being Seg b

( x in product F & HFG . x = Product x ) ) )

0 <> n0

then consider k0 being non zero Nat, a0 being k0 -element FinSequence of H, Inda0 being k0 -element FinSequence of NAT , F0 being Group-like associative commutative multMagma-Family of Seg k0, HFG0 being Homomorphism of (product F0),H such that

P12: ( ( for i being Nat st i in Seg k0 holds

ex ai being Element of H st

( ai = a0 . i & F0 . i = gr {ai} & ord ai = p |^ (Inda0 . i) ) ) & ( for i being Nat st 1 <= i & i <= k0 - 1 holds

Inda0 . i <= Inda0 . (i + 1) ) & ( for p, q being Element of Seg k0 st p <> q holds

the carrier of (F0 . p) /\ the carrier of (F0 . q) = {(1_ H)} ) & HFG0 is bijective & ( for x being Seg k0 -defined the carrier of H -valued total Function st ( for p being Element of Seg k0 holds x . p in F0 . p ) holds

( x in product F0 & HFG0 . x = Product x ) ) ) by P8, APN;

reconsider q = k0 + 1 as non zero Nat ;

set K = gr {g0};

set F = F0 +* ({q} --> (gr {g0}));

set I0 = Seg k0;

set I = Seg q;

INDK1: Inda0 . k0 <= n0

DIQ1: for x being object holds

( x in Seg k0 iff ( x in Seg q & not x in {q} ) )

NU1: not q in Seg k0

NU2: (Seg k0) \/ {q} = Seg q by DIQ0, XB1, XBOOLE_1:45;

<*g0*> is FinSequence of G by FINSEQ_1:74;

then VV1: rng <*g0*> c= the carrier of G by FINSEQ_1:def 4;

n0 is Element of NAT by ORDINAL1:def 12;

then <*n0*> is FinSequence of NAT by FINSEQ_1:74;

then VV2: rng <*n0*> c= NAT by FINSEQ_1:def 4;

the carrier of H c= the carrier of G by GROUP_2:def 5;

then VV4: rng a0 c= the carrier of G by XBOOLE_1:1;

rng (a0 ^ <*g0*>) = (rng a0) \/ (rng <*g0*>) by FINSEQ_1:31;

then reconsider a = a0 ^ <*g0*> as q -element FinSequence of G by VV1, VV4, XBOOLE_1:8, FINSEQ_1:def 4;

rng (Inda0 ^ <*n0*>) = (rng Inda0) \/ (rng <*n0*>) by FINSEQ_1:31;

then reconsider Inda = Inda0 ^ <*n0*> as q -element FinSequence of NAT by VV2, XBOOLE_1:8, FINSEQ_1:def 4;

LL1: len a0 = k0 by CARD_1:def 7;

LL2: len Inda0 = k0 by CARD_1:def 7;

EX1: for i being Nat st 1 <= i & i <= q - 1 holds

Inda . i <= Inda . (i + 1)

.= (Seg k0) \/ (dom ({q} --> (gr {g0}))) by PARTFUN1:def 2

.= (Seg k0) \/ {q} ;

then reconsider F = F0 +* ({q} --> (gr {g0})) as Seg q -defined Function by NU2, RELAT_1:def 18;

reconsider F = F as ManySortedSet of Seg q by NU2, PARTFUN1:def 2, D1;

for y being set st y in rng F holds

y is non empty multMagma

P12A: for x being Element of Seg k0 holds

( F0 . x is finite strict commutative Group & F0 . x is Subgroup of H )

ex ai being Element of G st

( ai = a . i & F . i = gr {ai} & ord ai = p |^ (Inda . i) )

( F . x is finite strict commutative Group & F . x is Subgroup of G )

AR2: for i being Element of Seg q holds F . i is associative by XPFA;

for i being Element of Seg q holds F . i is commutative by XPFA;

then reconsider F = F as Group-like associative commutative multMagma-Family of Seg q by AR1, GROUP_7:def 6, AR2, GROUP_7:def 7, GROUP_7:def 8;

consider FHKG being Homomorphism of (product <*H,(gr {g0})*>),G such that

XX1: ( FHKG is bijective & ( for a, b being Element of G st a in H & b in gr {g0} holds

FHKG . <*a,b*> = a * b ) ) by P8;

XF1: F = F0 +* (q .--> (gr {g0})) ;

then consider FHK being Homomorphism of (product F),(product <*H,(gr {g0})*>) such that

D7: ( FHK is bijective & ( for x0 being Function

for k being Element of (gr {g0})

for h being Element of H st h = HFG0 . x0 & x0 in product F0 holds

FHK . (x0 +* (q .--> k)) = <*h,k*> ) ) by GROUP_17:28, P12, NU0, NU2, NU1;

reconsider HFG = FHKG * FHK as Function of (product F),G ;

XX2: HFG is onto by FUNCT_2:27, XX1, D7;

reconsider HFG = HFG as Homomorphism of (product F),G ;

DX2: for x being Seg q -defined the carrier of G -valued total Function st ( for p being Element of Seg q holds x . p in F . p ) holds

( x in product F & HFG . x = Product x )

the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)}_{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 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 i, j being Element of Seg k st i <> j holds

the carrier of (F . i) /\ the carrier of (F . j) = {(1_ G)} ) & HFG is bijective & ( for 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 ) holds

( x in product F & HFG . x = Product x ) ) ) by EX1, XPF, XX2, XX1, D7, DX2; :: thesis: verum

end;proof

then
n - n0 < n - 0
by XREAL_1:15;
assume X0:
n0 = 0
; :: thesis: contradiction

then X1: ord g0 = 1 by P8, NEWTON:4;

for z being object holds

( z in the carrier of G iff z in {(1_ G)} )

n = 0

end;then X1: ord g0 = 1 by P8, NEWTON:4;

for z being object holds

( z in the carrier of G iff z in {(1_ G)} )

proof

then XX1:
the carrier of G = {(1_ G)}
by TARSKI:2;
let z be object ; :: thesis: ( z in the carrier of G iff z in {(1_ G)} )

hence z in the carrier of G ; :: thesis: verum

end;hereby :: thesis: ( z in {(1_ G)} implies z in the carrier of G )

assume
z in {(1_ G)}
; :: thesis: z in the carrier of Gassume
z in the carrier of G
; :: thesis: z in {(1_ G)}

then reconsider x = z as Element of G ;

ord x in Ordset G ;

then X2: ord x <= 1 by X1, P8, SEQ_4:def 1;

ord x = card (gr {x}) by GR_CY_1:7;

then 1 <= ord x by GROUP_1:45;

then x = 1_ G by X2, XXREAL_0:1, GROUP_1:43;

hence z in {(1_ G)} by TARSKI:def 1; :: thesis: verum

end;then reconsider x = z as Element of G ;

ord x in Ordset G ;

then X2: ord x <= 1 by X1, P8, SEQ_4:def 1;

ord x = card (gr {x}) by GR_CY_1:7;

then 1 <= ord x by GROUP_1:45;

then x = 1_ G by X2, XXREAL_0:1, GROUP_1:43;

hence z in {(1_ G)} by TARSKI:def 1; :: thesis: verum

hence z in the carrier of G ; :: thesis: verum

n = 0

proof

hence
contradiction
by X0, AAA; :: thesis: verum
assume
n <> 0
; :: thesis: contradiction

then 1 < p to_power n by POWER:35, INT_2:def 4;

hence contradiction by AS1, XX1, CARD_1:30; :: thesis: verum

end;then 1 < p to_power n by POWER:35, INT_2:def 4;

hence contradiction by AS1, XX1, CARD_1:30; :: thesis: verum

then consider k0 being non zero Nat, a0 being k0 -element FinSequence of H, Inda0 being k0 -element FinSequence of NAT , F0 being Group-like associative commutative multMagma-Family of Seg k0, HFG0 being Homomorphism of (product F0),H such that

P12: ( ( for i being Nat st i in Seg k0 holds

ex ai being Element of H st

( ai = a0 . i & F0 . i = gr {ai} & ord ai = p |^ (Inda0 . i) ) ) & ( for i being Nat st 1 <= i & i <= k0 - 1 holds

Inda0 . i <= Inda0 . (i + 1) ) & ( for p, q being Element of Seg k0 st p <> q holds

the carrier of (F0 . p) /\ the carrier of (F0 . q) = {(1_ H)} ) & HFG0 is bijective & ( for x being Seg k0 -defined the carrier of H -valued total Function st ( for p being Element of Seg k0 holds x . p in F0 . p ) holds

( x in product F0 & HFG0 . x = Product x ) ) ) by P8, APN;

reconsider q = k0 + 1 as non zero Nat ;

set K = gr {g0};

set F = F0 +* ({q} --> (gr {g0}));

set I0 = Seg k0;

set I = Seg q;

INDK1: Inda0 . k0 <= n0

proof

NU0:
q is Element of Seg q
by FINSEQ_1:4;
assume K1:
not Inda0 . k0 <= n0
; :: thesis: contradiction

K2: 1 <= k0 by NAT_1:14;

1 < p by INT_2:def 4;

then K3: p to_power n0 < p to_power (Inda0 . k0) by K1, POWER:39;

k0 in Seg k0 by K2;

then consider ai being Element of H such that

C5: ( ai = a0 . k0 & F0 . k0 = gr {ai} & ord ai = p |^ (Inda0 . k0) ) by P12;

reconsider aai = ai as Element of G by TARSKI:def 3, GROUP_2:def 5;

D54: gr {aai} = gr {ai} by GR_CY_2:3;

D55: ord aai = card (gr {ai}) by D54, GR_CY_1:7

.= p |^ (Inda0 . k0) by C5, GR_CY_1:7 ;

ord aai in Ordset G ;

hence contradiction by D55, K3, P8, SEQ_4:def 1; :: thesis: verum

end;K2: 1 <= k0 by NAT_1:14;

1 < p by INT_2:def 4;

then K3: p to_power n0 < p to_power (Inda0 . k0) by K1, POWER:39;

k0 in Seg k0 by K2;

then consider ai being Element of H such that

C5: ( ai = a0 . k0 & F0 . k0 = gr {ai} & ord ai = p |^ (Inda0 . k0) ) by P12;

reconsider aai = ai as Element of G by TARSKI:def 3, GROUP_2:def 5;

D54: gr {aai} = gr {ai} by GR_CY_2:3;

D55: ord aai = card (gr {ai}) by D54, GR_CY_1:7

.= p |^ (Inda0 . k0) by C5, GR_CY_1:7 ;

ord aai in Ordset G ;

hence contradiction by D55, K3, P8, SEQ_4:def 1; :: thesis: verum

DIQ1: for x being object holds

( x in Seg k0 iff ( x in Seg q & not x in {q} ) )

proof

then DIQ0:
Seg k0 = (Seg q) \ {q}
by XBOOLE_0:def 5;
let x be object ; :: thesis: ( x in Seg k0 iff ( x in Seg q & not x in {q} ) )

then reconsider x1 = x as Nat ;

X2: ( 1 <= x1 & x1 <= q ) by X1, FINSEQ_1:1;

x1 <> q by X1, TARSKI:def 1;

then x1 < k0 + 1 by X2, XXREAL_0:1;

then x1 <= k0 by NAT_1:13;

hence x in Seg k0 by X2; :: thesis: verum

end;hereby :: thesis: ( x in Seg q & not x in {q} implies x in Seg k0 )

assume X1:
( x in Seg q & not x in {q} )
; :: thesis: x in Seg k0assume X1:
x in Seg k0
; :: thesis: ( x in Seg q & not x in {q} )

then reconsider x1 = x as Nat ;

X4: k0 < k0 + 1 by NAT_1:16;

x1 <> k0 + 1 by X1, NAT_1:16, FINSEQ_1:1;

hence ( x in Seg q & not x in {q} ) by X1, X4, FINSEQ_1:5, TARSKI:def 1, TARSKI:def 3; :: thesis: verum

end;then reconsider x1 = x as Nat ;

X4: k0 < k0 + 1 by NAT_1:16;

x1 <> k0 + 1 by X1, NAT_1:16, FINSEQ_1:1;

hence ( x in Seg q & not x in {q} ) by X1, X4, FINSEQ_1:5, TARSKI:def 1, TARSKI:def 3; :: thesis: verum

then reconsider x1 = x as Nat ;

X2: ( 1 <= x1 & x1 <= q ) by X1, FINSEQ_1:1;

x1 <> q by X1, TARSKI:def 1;

then x1 < k0 + 1 by X2, XXREAL_0:1;

then x1 <= k0 by NAT_1:13;

hence x in Seg k0 by X2; :: thesis: verum

NU1: not q in Seg k0

proof

XB1:
{q} c= Seg q
by FINSEQ_1:4, ZFMISC_1:31;
assume
q in Seg k0
; :: thesis: contradiction

then ( q in Seg q & not q in {q} ) by DIQ1;

hence contradiction by TARSKI:def 1; :: thesis: verum

end;then ( q in Seg q & not q in {q} ) by DIQ1;

hence contradiction by TARSKI:def 1; :: thesis: verum

NU2: (Seg k0) \/ {q} = Seg q by DIQ0, XB1, XBOOLE_1:45;

<*g0*> is FinSequence of G by FINSEQ_1:74;

then VV1: rng <*g0*> c= the carrier of G by FINSEQ_1:def 4;

n0 is Element of NAT by ORDINAL1:def 12;

then <*n0*> is FinSequence of NAT by FINSEQ_1:74;

then VV2: rng <*n0*> c= NAT by FINSEQ_1:def 4;

the carrier of H c= the carrier of G by GROUP_2:def 5;

then VV4: rng a0 c= the carrier of G by XBOOLE_1:1;

rng (a0 ^ <*g0*>) = (rng a0) \/ (rng <*g0*>) by FINSEQ_1:31;

then reconsider a = a0 ^ <*g0*> as q -element FinSequence of G by VV1, VV4, XBOOLE_1:8, FINSEQ_1:def 4;

rng (Inda0 ^ <*n0*>) = (rng Inda0) \/ (rng <*n0*>) by FINSEQ_1:31;

then reconsider Inda = Inda0 ^ <*n0*> as q -element FinSequence of NAT by VV2, XBOOLE_1:8, FINSEQ_1:def 4;

LL1: len a0 = k0 by CARD_1:def 7;

LL2: len Inda0 = k0 by CARD_1:def 7;

EX1: for i being Nat st 1 <= i & i <= q - 1 holds

Inda . i <= Inda . (i + 1)

proof

D1: dom (F0 +* ({q} --> (gr {g0}))) =
(dom F0) \/ (dom ({q} --> (gr {g0})))
by FUNCT_4:def 1
let i be Nat; :: thesis: ( 1 <= i & i <= q - 1 implies Inda . i <= Inda . (i + 1) )

assume EX11: ( 1 <= i & i <= q - 1 ) ; :: thesis: Inda . i <= Inda . (i + 1)

EX13: dom Inda0 = Seg k0 by LL2, FINSEQ_1:def 3;

1 <= k0 by NAT_1:14;

then k0 - 1 in NAT by INT_1:3, XREAL_1:48;

then reconsider k01 = k0 - 1 as Nat ;

end;assume EX11: ( 1 <= i & i <= q - 1 ) ; :: thesis: Inda . i <= Inda . (i + 1)

EX13: dom Inda0 = Seg k0 by LL2, FINSEQ_1:def 3;

1 <= k0 by NAT_1:14;

then k0 - 1 in NAT by INT_1:3, XREAL_1:48;

then reconsider k01 = k0 - 1 as Nat ;

per cases
( i <> q - 1 or i = q - 1 )
;

end;

suppose C1:
i <> q - 1
; :: thesis: Inda . i <= Inda . (i + 1)

then
i < k0
by EX11, XXREAL_0:1;

then C2: i + 1 <= (k0 - 1) + 1 by NAT_1:13;

i < k01 + 1 by C1, EX11, XXREAL_0:1;

then C6: i <= k01 by NAT_1:13;

i in Seg k0 by EX11;

then D56: Inda . i = Inda0 . i by EX13, FINSEQ_1:def 7;

1 <= i + 1 by NAT_1:11;

then i + 1 in Seg k0 by C2;

then Inda . (i + 1) = Inda0 . (i + 1) by EX13, FINSEQ_1:def 7;

hence Inda . i <= Inda . (i + 1) by D56, P12, C6, EX11; :: thesis: verum

end;then C2: i + 1 <= (k0 - 1) + 1 by NAT_1:13;

i < k01 + 1 by C1, EX11, XXREAL_0:1;

then C6: i <= k01 by NAT_1:13;

i in Seg k0 by EX11;

then D56: Inda . i = Inda0 . i by EX13, FINSEQ_1:def 7;

1 <= i + 1 by NAT_1:11;

then i + 1 in Seg k0 by C2;

then Inda . (i + 1) = Inda0 . (i + 1) by EX13, FINSEQ_1:def 7;

hence Inda . i <= Inda . (i + 1) by D56, P12, C6, EX11; :: thesis: verum

.= (Seg k0) \/ (dom ({q} --> (gr {g0}))) by PARTFUN1:def 2

.= (Seg k0) \/ {q} ;

then reconsider F = F0 +* ({q} --> (gr {g0})) as Seg q -defined Function by NU2, RELAT_1:def 18;

reconsider F = F as ManySortedSet of Seg q by NU2, PARTFUN1:def 2, D1;

for y being set st y in rng F holds

y is non empty multMagma

proof

then reconsider F = F as multMagma-Family of Seg q by GROUP_7:def 1;
let y be set ; :: thesis: ( y in rng F implies y is non empty multMagma )

assume y in rng F ; :: thesis: y is non empty multMagma

then consider x being object such that

D4: ( x in dom F & y = F . x ) by FUNCT_1:def 3;

F5: x in (dom F0) \/ (dom ({q} --> (gr {g0}))) by D4, FUNCT_4:def 1;

end;assume y in rng F ; :: thesis: y is non empty multMagma

then consider x being object such that

D4: ( x in dom F & y = F . x ) by FUNCT_1:def 3;

F5: x in (dom F0) \/ (dom ({q} --> (gr {g0}))) by D4, FUNCT_4:def 1;

per cases
( x in Seg k0 or x in {q} )
by XBOOLE_0:def 3, D4, D1;

end;

suppose D51:
x in Seg k0
; :: thesis: y is non empty multMagma

then
not x in dom ({q} --> (gr {g0}))
by DIQ1;

then D52: F . x = F0 . x by FUNCT_4:def 1, F5;

x in dom F0 by D51, PARTFUN1:def 2;

then F0 . x in rng F0 by FUNCT_1:3;

hence y is non empty multMagma by D52, D4, GROUP_7:def 1; :: thesis: verum

end;then D52: F . x = F0 . x by FUNCT_4:def 1, F5;

x in dom F0 by D51, PARTFUN1:def 2;

then F0 . x in rng F0 by FUNCT_1:3;

hence y is non empty multMagma by D52, D4, GROUP_7:def 1; :: thesis: verum

P12A: for x being Element of Seg k0 holds

( F0 . x is finite strict commutative Group & F0 . x is Subgroup of H )

proof

XPF:
for i being Nat st i in Seg q holds
let x be Element of Seg k0; :: thesis: ( F0 . x is finite strict commutative Group & F0 . x is Subgroup of H )

reconsider i = x as Nat ;

consider ai being Element of H such that

X1: ( ai = a0 . i & F0 . i = gr {ai} & ord ai = p |^ (Inda0 . i) ) by P12;

thus ( F0 . x is finite strict commutative Group & F0 . x is Subgroup of H ) by X1; :: thesis: verum

end;reconsider i = x as Nat ;

consider ai being Element of H such that

X1: ( ai = a0 . i & F0 . i = gr {ai} & ord ai = p |^ (Inda0 . i) ) by P12;

thus ( F0 . x is finite strict commutative Group & F0 . x is Subgroup of H ) by X1; :: thesis: verum

ex ai being Element of G st

( ai = a . i & F . i = gr {ai} & ord ai = p |^ (Inda . i) )

proof

XPFA:
for x being Element of Seg q holds
let i be Nat; :: thesis: ( i in Seg q implies ex ai being Element of G st

( ai = a . i & F . i = gr {ai} & ord ai = p |^ (Inda . i) ) )

assume DD: i in Seg q ; :: thesis: ex ai being Element of G st

( ai = a . i & F . i = gr {ai} & ord ai = p |^ (Inda . i) )

F5: i in (dom F0) \/ (dom ({q} --> (gr {g0}))) by D1, DD, NU2, FUNCT_4:def 1;

end;( ai = a . i & F . i = gr {ai} & ord ai = p |^ (Inda . i) ) )

assume DD: i in Seg q ; :: thesis: ex ai being Element of G st

( ai = a . i & F . i = gr {ai} & ord ai = p |^ (Inda . i) )

F5: i in (dom F0) \/ (dom ({q} --> (gr {g0}))) by D1, DD, NU2, FUNCT_4:def 1;

per cases
( i in Seg k0 or i in {q} )
by DD, NU2, XBOOLE_0:def 3;

end;

suppose D51:
i in Seg k0
; :: thesis: ex ai being Element of G st

( ai = a . i & F . i = gr {ai} & ord ai = p |^ (Inda . i) )

( ai = a . i & F . i = gr {ai} & ord ai = p |^ (Inda . i) )

then
not i in dom ({q} --> (gr {g0}))
by DIQ1;

then D52: F . i = F0 . i by F5, FUNCT_4:def 1;

consider ai being Element of H such that

D53: ( ai = a0 . i & F0 . i = gr {ai} & ord ai = p |^ (Inda0 . i) ) by P12, D51;

ai in H ;

then reconsider aai = ai as Element of G by GROUP_2:40, STRUCT_0:def 5;

D54: gr {aai} = gr {ai} by GR_CY_2:3;

D55: ord aai = card (gr {aai}) by GR_CY_1:7

.= ord ai by D54, GR_CY_1:7 ;

dom Inda0 = Seg k0 by LL2, FINSEQ_1:def 3;

then D56: Inda . i = Inda0 . i by D51, FINSEQ_1:def 7;

dom a0 = Seg k0 by LL1, FINSEQ_1:def 3;

then a . i = a0 . i by D51, FINSEQ_1:def 7;

hence ex ai being Element of G st

( ai = a . i & F . i = gr {ai} & ord ai = p |^ (Inda . i) ) by D52, D53, D54, D55, D56; :: thesis: verum

end;then D52: F . i = F0 . i by F5, FUNCT_4:def 1;

consider ai being Element of H such that

D53: ( ai = a0 . i & F0 . i = gr {ai} & ord ai = p |^ (Inda0 . i) ) by P12, D51;

ai in H ;

then reconsider aai = ai as Element of G by GROUP_2:40, STRUCT_0:def 5;

D54: gr {aai} = gr {ai} by GR_CY_2:3;

D55: ord aai = card (gr {aai}) by GR_CY_1:7

.= ord ai by D54, GR_CY_1:7 ;

dom Inda0 = Seg k0 by LL2, FINSEQ_1:def 3;

then D56: Inda . i = Inda0 . i by D51, FINSEQ_1:def 7;

dom a0 = Seg k0 by LL1, FINSEQ_1:def 3;

then a . i = a0 . i by D51, FINSEQ_1:def 7;

hence ex ai being Element of G st

( ai = a . i & F . i = gr {ai} & ord ai = p |^ (Inda . i) ) by D52, D53, D54, D55, D56; :: thesis: verum

suppose D52:
i in {q}
; :: thesis: ex ai being Element of G st

( ai = a . i & F . i = gr {ai} & ord ai = p |^ (Inda . i) )

( ai = a . i & F . i = gr {ai} & ord ai = p |^ (Inda . i) )

D55: F . i =
({q} --> (gr {g0})) . i
by FUNCT_4:def 1, F5, D52

.= gr {g0} by D52, FUNCOP_1:7 ;

D56: i = q by TARSKI:def 1, D52;

D57: a . i = g0 by LL1, FINSEQ_1:42, D56;

ord g0 = p |^ (Inda . i) by P8, D56, LL2, FINSEQ_1:42;

hence ex ai being Element of G st

( ai = a . i & F . i = gr {ai} & ord ai = p |^ (Inda . i) ) by D55, D57; :: thesis: verum

end;.= gr {g0} by D52, FUNCOP_1:7 ;

D56: i = q by TARSKI:def 1, D52;

D57: a . i = g0 by LL1, FINSEQ_1:42, D56;

ord g0 = p |^ (Inda . i) by P8, D56, LL2, FINSEQ_1:42;

hence ex ai being Element of G st

( ai = a . i & F . i = gr {ai} & ord ai = p |^ (Inda . i) ) by D55, D57; :: thesis: verum

( F . x is finite strict commutative Group & F . x is Subgroup of G )

proof

AR1:
for i being Element of Seg q holds F . i is Group-like
by XPFA;
let x be Element of Seg q; :: thesis: ( F . x is finite strict commutative Group & F . x is Subgroup of G )

reconsider i = x as Nat ;

consider ai being Element of G such that

X1: ( ai = a . i & F . i = gr {ai} & ord ai = p |^ (Inda . i) ) by XPF;

thus ( F . x is finite strict commutative Group & F . x is Subgroup of G ) by X1; :: thesis: verum

end;reconsider i = x as Nat ;

consider ai being Element of G such that

X1: ( ai = a . i & F . i = gr {ai} & ord ai = p |^ (Inda . i) ) by XPF;

thus ( F . x is finite strict commutative Group & F . x is Subgroup of G ) by X1; :: thesis: verum

AR2: for i being Element of Seg q holds F . i is associative by XPFA;

for i being Element of Seg q holds F . i is commutative by XPFA;

then reconsider F = F as Group-like associative commutative multMagma-Family of Seg q by AR1, GROUP_7:def 6, AR2, GROUP_7:def 7, GROUP_7:def 8;

consider FHKG being Homomorphism of (product <*H,(gr {g0})*>),G such that

XX1: ( FHKG is bijective & ( for a, b being Element of G st a in H & b in gr {g0} holds

FHKG . <*a,b*> = a * b ) ) by P8;

XF1: F = F0 +* (q .--> (gr {g0})) ;

then consider FHK being Homomorphism of (product F),(product <*H,(gr {g0})*>) such that

D7: ( FHK is bijective & ( for x0 being Function

for k being Element of (gr {g0})

for h being Element of H st h = HFG0 . x0 & x0 in product F0 holds

FHK . (x0 +* (q .--> k)) = <*h,k*> ) ) by GROUP_17:28, P12, NU0, NU2, NU1;

reconsider HFG = FHKG * FHK as Function of (product F),G ;

XX2: HFG is onto by FUNCT_2:27, XX1, D7;

reconsider HFG = HFG as Homomorphism of (product F),G ;

DX2: for x being Seg q -defined the carrier of G -valued total Function st ( for p being Element of Seg q holds x . p in F . p ) holds

( x in product F & HFG . x = Product x )

proof

for s, t being Element of Seg q st s <> t holds
let x be Seg q -defined the carrier of G -valued total Function; :: thesis: ( ( for p being Element of Seg q holds x . p in F . p ) implies ( x in product F & HFG . x = Product x ) )

assume U1: for p being Element of Seg q holds x . p in F . p ; :: thesis: ( x in product F & HFG . x = Product x )

then x in the carrier of (product F) by GROUP_17:29;

then consider x0 being Seg k0 -defined total Function, k being Element of (gr {g0}) such that

U3: ( x0 in product F0 & x = x0 +* (q .--> k) & ( for p being Element of Seg k0 holds x0 . p in F0 . p ) ) by XF1, GROUP_17:30, NU2, NU1, NU0;

reconsider h = HFG0 . x0 as Element of H by FUNCT_2:5, U3;

reconsider hh = h, kk = k as Element of G by GROUP_2:42;

U5: HFG0 . x0 = Product x0 by P12, U3;

the carrier of H c= the carrier of G by GROUP_2:def 5;

then rng x0 c= the carrier of G by XBOOLE_1:1;

then reconsider xx0 = x0 as Seg k0 -defined the carrier of G -valued total Function by RELAT_1:def 19;

U50: Product x0 = Product xx0 by GROUP_17:32;

thus x in product F by GROUP_17:29, U1; :: thesis: HFG . x = Product x

U6: ( hh in H & kk in gr {g0} ) ;

thus HFG . x = FHKG . (FHK . x) by FUNCT_2:15, GROUP_17:29, U1

.= FHKG . <*hh,kk*> by D7, U3

.= hh * kk by XX1, U6

.= Product x by U5, U50, NU0, NU2, NU1, GROUP_17:33, U3 ; :: thesis: verum

end;assume U1: for p being Element of Seg q holds x . p in F . p ; :: thesis: ( x in product F & HFG . x = Product x )

then x in the carrier of (product F) by GROUP_17:29;

then consider x0 being Seg k0 -defined total Function, k being Element of (gr {g0}) such that

U3: ( x0 in product F0 & x = x0 +* (q .--> k) & ( for p being Element of Seg k0 holds x0 . p in F0 . p ) ) by XF1, GROUP_17:30, NU2, NU1, NU0;

reconsider h = HFG0 . x0 as Element of H by FUNCT_2:5, U3;

reconsider hh = h, kk = k as Element of G by GROUP_2:42;

now :: thesis: for y being object st y in rng x0 holds

y in the carrier of H

then reconsider x0 = x0 as Seg k0 -defined the carrier of H -valued total Function by RELAT_1:def 19, TARSKI:def 3;y in the carrier of H

let y be object ; :: thesis: ( y in rng x0 implies y in the carrier of H )

assume y in rng x0 ; :: thesis: y in the carrier of H

then consider z being object such that

DX11: ( z in dom x0 & y = x0 . z ) by FUNCT_1:def 3;

reconsider z = z as Element of Seg k0 by DX11;

DX13: x0 . z in F0 . z by U3;

F0 . z is Subgroup of H by P12A;

hence y in the carrier of H by DX11, STRUCT_0:def 5, DX13, GROUP_2:40; :: thesis: verum

end;assume y in rng x0 ; :: thesis: y in the carrier of H

then consider z being object such that

DX11: ( z in dom x0 & y = x0 . z ) by FUNCT_1:def 3;

reconsider z = z as Element of Seg k0 by DX11;

DX13: x0 . z in F0 . z by U3;

F0 . z is Subgroup of H by P12A;

hence y in the carrier of H by DX11, STRUCT_0:def 5, DX13, GROUP_2:40; :: thesis: verum

U5: HFG0 . x0 = Product x0 by P12, U3;

the carrier of H c= the carrier of G by GROUP_2:def 5;

then rng x0 c= the carrier of G by XBOOLE_1:1;

then reconsider xx0 = x0 as Seg k0 -defined the carrier of G -valued total Function by RELAT_1:def 19;

U50: Product x0 = Product xx0 by GROUP_17:32;

thus x in product F by GROUP_17:29, U1; :: thesis: HFG . x = Product x

U6: ( hh in H & kk in gr {g0} ) ;

thus HFG . x = FHKG . (FHK . x) by FUNCT_2:15, GROUP_17:29, U1

.= FHKG . <*hh,kk*> by D7, U3

.= hh * kk by XX1, U6

.= Product x by U5, U50, NU0, NU2, NU1, GROUP_17:33, U3 ; :: thesis: verum

the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)}

proof

hence
ex k being non zero Nat ex a being b
let s, t be Element of Seg q; :: thesis: ( s <> t implies the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)} )

assume AA1: s <> t ; :: thesis: the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)}

dom F = Seg q by PARTFUN1:def 2;

then D4: ( s in dom F & t in dom F ) ;

end;assume AA1: s <> t ; :: thesis: the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)}

dom F = Seg q by PARTFUN1:def 2;

then D4: ( s in dom F & t in dom F ) ;

per cases
( ( s in Seg k0 & t in Seg k0 ) or not s in Seg k0 or not t in Seg k0 )
;

end;

suppose
( s in Seg k0 & t in Seg k0 )
; :: thesis: the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)}

then reconsider ss = s, tt = t as Element of Seg k0 ;

F5: s in (dom F0) \/ (dom ({q} --> (gr {g0}))) by D4, FUNCT_4:def 1;

K5: t in (dom F0) \/ (dom ({q} --> (gr {g0}))) by D4, FUNCT_4:def 1;

not ss in dom ({q} --> (gr {g0})) by DIQ1;

then D52: F . ss = F0 . ss by FUNCT_4:def 1, F5;

not tt in dom ({q} --> (gr {g0})) by DIQ1;

then K52: F . tt = F0 . tt by FUNCT_4:def 1, K5;

the carrier of (F0 . ss) /\ the carrier of (F0 . tt) = {(1_ H)} by P12, AA1;

hence the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)} by D52, K52, GROUP_2:44; :: thesis: verum

end;F5: s in (dom F0) \/ (dom ({q} --> (gr {g0}))) by D4, FUNCT_4:def 1;

K5: t in (dom F0) \/ (dom ({q} --> (gr {g0}))) by D4, FUNCT_4:def 1;

not ss in dom ({q} --> (gr {g0})) by DIQ1;

then D52: F . ss = F0 . ss by FUNCT_4:def 1, F5;

not tt in dom ({q} --> (gr {g0})) by DIQ1;

then K52: F . tt = F0 . tt by FUNCT_4:def 1, K5;

the carrier of (F0 . ss) /\ the carrier of (F0 . tt) = {(1_ H)} by P12, AA1;

hence the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)} by D52, K52, GROUP_2:44; :: thesis: verum

suppose AA3:
( not s in Seg k0 or not t in Seg k0 )
; :: thesis: the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)}

thus
the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)}
:: thesis: verum

end;proof
end;

per cases
( not s in Seg k0 or not t in Seg k0 )
by AA3;

end;

suppose AA31:
not s in Seg k0
; :: thesis: the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)}

F5:
s in (dom F0) \/ (dom ({q} --> (gr {g0})))
by D4, FUNCT_4:def 1;

D52: s in {q} by AA31, DIQ1;

then F . s = ({q} --> (gr {g0})) . s by FUNCT_4:def 1, F5;

then D55: F . s = gr {g0} by D52, FUNCOP_1:7;

t in Seg k0

K5: tt in (dom F0) \/ (dom ({q} --> (gr {g0}))) by D4, FUNCT_4:def 1;

not tt in dom ({q} --> (gr {g0})) by DIQ1;

then K52: F . tt = F0 . tt by FUNCT_4:def 1, K5;

reconsider S1 = F0 . tt as Subgroup of H by P12A;

K55: the carrier of (gr {g0}) /\ the carrier of S1 c= {(1_ G)} by P8, XBOOLE_1:26, GROUP_2:def 5;

K56: 1_ G in the carrier of (gr {g0}) by GROUP_2:46, STRUCT_0:def 5;

1_ G in the carrier of S1 by GROUP_2:46, STRUCT_0:def 5;

then 1_ G in the carrier of (gr {g0}) /\ the carrier of S1 by XBOOLE_0:def 4, K56;

then {(1_ G)} c= the carrier of (gr {g0}) /\ the carrier of S1 by ZFMISC_1:31;

hence the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)} by D55, K52, K55, XBOOLE_0:def 10; :: thesis: verum

end;D52: s in {q} by AA31, DIQ1;

then F . s = ({q} --> (gr {g0})) . s by FUNCT_4:def 1, F5;

then D55: F . s = gr {g0} by D52, FUNCOP_1:7;

t in Seg k0

proof

then reconsider tt = t as Element of Seg k0 ;
assume
not t in Seg k0
; :: thesis: contradiction

then ( not t in Seg q or t in {q} ) by DIQ1;

then t = q by TARSKI:def 1;

hence contradiction by AA1, TARSKI:def 1, D52; :: thesis: verum

end;then ( not t in Seg q or t in {q} ) by DIQ1;

then t = q by TARSKI:def 1;

hence contradiction by AA1, TARSKI:def 1, D52; :: thesis: verum

K5: tt in (dom F0) \/ (dom ({q} --> (gr {g0}))) by D4, FUNCT_4:def 1;

not tt in dom ({q} --> (gr {g0})) by DIQ1;

then K52: F . tt = F0 . tt by FUNCT_4:def 1, K5;

reconsider S1 = F0 . tt as Subgroup of H by P12A;

K55: the carrier of (gr {g0}) /\ the carrier of S1 c= {(1_ G)} by P8, XBOOLE_1:26, GROUP_2:def 5;

K56: 1_ G in the carrier of (gr {g0}) by GROUP_2:46, STRUCT_0:def 5;

1_ G in the carrier of S1 by GROUP_2:46, STRUCT_0:def 5;

then 1_ G in the carrier of (gr {g0}) /\ the carrier of S1 by XBOOLE_0:def 4, K56;

then {(1_ G)} c= the carrier of (gr {g0}) /\ the carrier of S1 by ZFMISC_1:31;

hence the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)} by D55, K52, K55, XBOOLE_0:def 10; :: thesis: verum

suppose AA32:
not t in Seg k0
; :: thesis: the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)}

F5:
t in (dom F0) \/ (dom ({q} --> (gr {g0})))
by D4, FUNCT_4:def 1;

D52: t in {q} by AA32, DIQ1;

then F . t = ({q} --> (gr {g0})) . t by FUNCT_4:def 1, F5;

then D55: F . t = gr {g0} by D52, FUNCOP_1:7;

s in Seg k0

K5: ss in (dom F0) \/ (dom ({q} --> (gr {g0}))) by D4, FUNCT_4:def 1;

not ss in dom ({q} --> (gr {g0})) by DIQ1;

then K52: F . ss = F0 . ss by FUNCT_4:def 1, K5;

reconsider S1 = F0 . ss as Subgroup of H by P12A;

K55: the carrier of (gr {g0}) /\ the carrier of S1 c= {(1_ G)} by P8, XBOOLE_1:26, GROUP_2:def 5;

K56: 1_ G in the carrier of (gr {g0}) by GROUP_2:46, STRUCT_0:def 5;

1_ G in the carrier of S1 by GROUP_2:46, STRUCT_0:def 5;

then 1_ G in the carrier of (gr {g0}) /\ the carrier of S1 by XBOOLE_0:def 4, K56;

then {(1_ G)} c= the carrier of (gr {g0}) /\ the carrier of S1 by ZFMISC_1:31;

hence the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)} by D55, K52, K55, XBOOLE_0:def 10; :: thesis: verum

end;D52: t in {q} by AA32, DIQ1;

then F . t = ({q} --> (gr {g0})) . t by FUNCT_4:def 1, F5;

then D55: F . t = gr {g0} by D52, FUNCOP_1:7;

s in Seg k0

proof

then reconsider ss = s as Element of Seg k0 ;
assume
not s in Seg k0
; :: thesis: contradiction

then ( not s in Seg q or s in {q} ) by DIQ1;

then s = q by TARSKI:def 1;

hence contradiction by AA1, TARSKI:def 1, D52; :: thesis: verum

end;then ( not s in Seg q or s in {q} ) by DIQ1;

then s = q by TARSKI:def 1;

hence contradiction by AA1, TARSKI:def 1, D52; :: thesis: verum

K5: ss in (dom F0) \/ (dom ({q} --> (gr {g0}))) by D4, FUNCT_4:def 1;

not ss in dom ({q} --> (gr {g0})) by DIQ1;

then K52: F . ss = F0 . ss by FUNCT_4:def 1, K5;

reconsider S1 = F0 . ss as Subgroup of H by P12A;

K55: the carrier of (gr {g0}) /\ the carrier of S1 c= {(1_ G)} by P8, XBOOLE_1:26, GROUP_2:def 5;

K56: 1_ G in the carrier of (gr {g0}) by GROUP_2:46, STRUCT_0:def 5;

1_ G in the carrier of S1 by GROUP_2:46, STRUCT_0:def 5;

then 1_ G in the carrier of (gr {g0}) /\ the carrier of S1 by XBOOLE_0:def 4, K56;

then {(1_ G)} c= the carrier of (gr {g0}) /\ the carrier of S1 by ZFMISC_1:31;

hence the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)} by D55, K52, K55, XBOOLE_0:def 10; :: 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 i, j being Element of Seg k st i <> j holds

the carrier of (F . i) /\ the carrier of (F . j) = {(1_ G)} ) & HFG is bijective & ( for x being Seg b

( x in product F & HFG . x = Product x ) ) ) by EX1, XPF, XX2, XX1, D7, DX2; :: thesis: verum

hence 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

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

( x in product F & HFG . x = Product x ) ) ) ; :: thesis: verum