defpred S₁[ 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₃ -element FinSequence of G ex Inda being b₃ -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₃ -defined the carrier of b₁ -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₁[k] ) holds
S₁[n]

let n be Nat; :: thesis:
assume APN: for k being Nat st k < n holds
S₁[k] ; :: thesis:
thus S₁[n] :: thesis:

let G be finite strict commutative Group; :: thesis:
let p be Prime; :: thesis:
assume AS1: card G = p |^ n ; :: thesis:
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 ;

suppose BBB: n = n0 ; :: thesis:

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

proof

let i be Nat; :: thesis:
assume ASD1: i in Seg q ; :: thesis:
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:

end;

Z2: for i being Nat st 1 <= i & i <= q - 1 holds
Inda . i <= Inda . (i + 1)

proof

let i be Nat; :: thesis:
assume ( 1 <= i & i <= q - 1 ) ; :: thesis:
then ( 1 <= i & i <= 0 ) ;
hence Inda . i <= Inda . (i + 1) ; :: thesis:

end;

for y being set st y in rng ({q} --> G) holds
y is non empty multMagma

proof

let y be set ; :: thesis:
assume y in rng ({q} --> G) ; :: thesis:
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:

end;

then reconsider F = {q} --> G as multMagma-Family of {q} by GROUP_7:def 1;
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

let s, t be Element of {q}; :: thesis:
assume GG11: s <> t ; :: thesis:
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:

end;

AR1: for i being Element of {q} holds F . i is Group-like ;
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₁ -element FinSequence of G ex Inda being b₁ -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₁ -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:

end;

suppose AAA: n <> n0 ; :: thesis:

0 <> n0

proof

assume X0: n0 = 0 ; :: thesis:
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

let z be object ; :: thesis:

hereby :: thesis:

assume z in the carrier of G ; :: thesis:
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:

end;

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

end;

then XX1: the carrier of G = {(1_ G)} by TARSKI:2;
n = 0

proof

assume n <> 0 ; :: thesis:
then 1 < p to_power n by POWER:35, INT_2:def 4;
hence contradiction by AS1, XX1, CARD_1:30; :: thesis:

end;

hence contradiction by X0, AAA; :: thesis:

end;

then n - n0 < n - 0 by XREAL_1:15;
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

assume K1: not Inda0 . k0 <= n0 ; :: thesis:
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:

end;

NU0: q is Element of Seg q by FINSEQ_1:4;
DIQ1: for x being object holds
( x in Seg k0 iff ( x in Seg q & not x in {q} ) )

proof

let x be object ; :: thesis:

hereby :: thesis:

assume X1: x in Seg k0 ; :: thesis:
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:

end;

assume X1: ( x in Seg q & not x in {q} ) ; :: thesis:
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:

end;

then DIQ0: Seg k0 = (Seg q) \ {q} by XBOOLE_0:def 5;
NU1: not q in Seg k0

proof

assume q in Seg k0 ; :: thesis:
then ( q in Seg q & not q in {q} ) by DIQ1;
hence contradiction by TARSKI:def 1; :: thesis:

end;

XB1: {q} c= Seg q by FINSEQ_1:4, ZFMISC_1:31;
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

let i be Nat; :: thesis:
assume EX11: ( 1 <= i & i <= q - 1 ) ; :: thesis:
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 ;

suppose C1: i <> q - 1 ; :: thesis:

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:

end;

suppose C2: i = q - 1 ; :: thesis:

i in Seg k0 by EX11;
then Inda . i = Inda0 . i by EX13, FINSEQ_1:def 7;
hence Inda . i <= Inda . (i + 1) by C2, INDK1, LL2, FINSEQ_1:42; :: thesis:

end;

D1: dom (F0 +* ({q} --> (gr {g0}))) = (dom F0) \/ (dom ({q} --> (gr {g0}))) by FUNCT_4:def 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

proof

let y be set ; :: thesis:
assume y in rng F ; :: thesis:
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 by XBOOLE_0:def 3, D4, D1;

suppose D51: x in Seg k0 ; :: thesis:

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:

end;

suppose D52: x in {q} ; :: thesis:

then F . x = ({q} --> (gr {g0})) . x by FUNCT_4:def 1, F5;
hence y is non empty multMagma by D4, D52, FUNCOP_1:7; :: thesis:

end;

then reconsider F = F as multMagma-Family of Seg q by GROUP_7:def 1;
P12A: for x being Element of Seg k0 holds
( F0 . x is finite strict commutative Group & F0 . x is Subgroup of H )

proof

let x be Element of Seg k0; :: thesis:
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:

end;

XPF: for i being Nat st i in Seg q holds
ex ai being Element of G st
( ai = a . i & F . i = gr {ai} & ord ai = p |^ (Inda . i) )

proof

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

per cases by DD, NU2, XBOOLE_0:def 3;

suppose D51: i in Seg k0 ; :: thesis:

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:

end;

suppose D52: i in {q} ; :: thesis:

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:

end;

XPFA: for x being Element of Seg q holds
( F . x is finite strict commutative Group & F . x is Subgroup of G )

proof

let x be Element of Seg q; :: thesis:
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:

end;

AR1: for i being Element of Seg q holds F . i is Group-like by XPFA;
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

let x be Seg q -defined the carrier of G -valued total Function; :: thesis:
assume U1: for p being Element of Seg q holds x . p in F . p ; :: thesis:
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:

let y be object ; :: thesis:
assume y in rng x0 ; :: thesis:
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:

end;

then reconsider x0 = x0 as Seg k0 -defined the carrier of H -valued total Function by RELAT_1:def 19, TARSKI:def 3;
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:
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:

end;

for s, t being Element of Seg q st s <> t holds
the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)}

proof

let s, t be Element of Seg q; :: thesis:
assume AA1: s <> t ; :: thesis:
dom F = Seg q by PARTFUN1:def 2;
then D4: ( s in dom F & t in dom F ) ;

per cases ;

suppose ( s in Seg k0 & t in Seg k0 ) ; :: thesis:

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:

end;

suppose AA3: ( not s in Seg k0 or not t in Seg k0 ) ; :: thesis:

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

proof

per cases by AA3;

suppose AA31: not s in Seg k0 ; :: thesis:

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

proof

assume not t in Seg k0 ; :: thesis:
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:

end;

then reconsider tt = t as Element of 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:

end;

suppose AA32: not t in Seg k0 ; :: thesis:

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

proof

assume not s in Seg k0 ; :: thesis:
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:

end;

then reconsider ss = s as Element of 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:

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 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₁ -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:

end;

for k being Nat holds S₁[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₄ -element FinSequence of G ex Inda being b₄ -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₄ -defined the carrier of b₁ -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: