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

for p being Prime

for g being Element of G st card G = p |^ $1 & ord g = upper_bound (Ordset G) holds

ex K being strict normal Subgroup of G st

( the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {g} & x = b1 * a1 ) ) );

P0: S_{1}[ 0 ]
_{1}[k] holds

S_{1}[k + 1]
_{1}[k]
from NAT_1:sch 2(P0, PN);

hence for G being finite strict commutative Group

for p being Prime

for m being Nat

for g being Element of G st card G = p |^ m & ord g = upper_bound (Ordset G) holds

ex K being strict normal Subgroup of G st

( the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {g} & x = b1 * a1 ) ) ) ; :: thesis: verum

for p being Prime

for g being Element of G st card G = p |^ $1 & ord g = upper_bound (Ordset G) holds

ex K being strict normal Subgroup of G st

( the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {g} & x = b1 * a1 ) ) );

P0: S

proof

PN:
for k being Nat st S
let G be finite strict commutative Group; :: thesis: for p being Prime

for g being Element of G st card G = p |^ 0 & ord g = upper_bound (Ordset G) holds

ex K being strict normal Subgroup of G st

( the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {g} & x = b1 * a1 ) ) )

let p be Prime; :: thesis: for g being Element of G st card G = p |^ 0 & ord g = upper_bound (Ordset G) holds

ex K being strict normal Subgroup of G st

( the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {g} & x = b1 * a1 ) ) )

let g be Element of G; :: thesis: ( card G = p |^ 0 & ord g = upper_bound (Ordset G) implies ex K being strict normal Subgroup of G st

( the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {g} & x = b1 * a1 ) ) ) )

assume AS1: ( card G = p |^ 0 & ord g = upper_bound (Ordset G) ) ; :: thesis: ex K being strict normal Subgroup of G st

( the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {g} & x = b1 * a1 ) ) )

reconsider H = G as finite strict Subgroup of G by GROUP_2:54;

card H = 1 by AS1, NEWTON:4;

then A1: (1). G = G by GROUP_2:70;

reconsider K = (1). G as strict normal Subgroup of G ;

g in the carrier of ((1). G) by A1;

then g in {(1_ G)} by GROUP_2:def 7;

then A2: g = 1_ G by TARSKI:def 1;

for x being object holds

( x in the carrier of (gr {g}) iff x in {(1_ G)} )

the carrier of K = {(1_ G)} by GROUP_2:def 7;

then X2: the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} by X1;

for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {g} & x = b1 * a1 )

( the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {g} & x = b1 * a1 ) ) ) by X2; :: thesis: verum

end;for g being Element of G st card G = p |^ 0 & ord g = upper_bound (Ordset G) holds

ex K being strict normal Subgroup of G st

( the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {g} & x = b1 * a1 ) ) )

let p be Prime; :: thesis: for g being Element of G st card G = p |^ 0 & ord g = upper_bound (Ordset G) holds

ex K being strict normal Subgroup of G st

( the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {g} & x = b1 * a1 ) ) )

let g be Element of G; :: thesis: ( card G = p |^ 0 & ord g = upper_bound (Ordset G) implies ex K being strict normal Subgroup of G st

( the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {g} & x = b1 * a1 ) ) ) )

assume AS1: ( card G = p |^ 0 & ord g = upper_bound (Ordset G) ) ; :: thesis: ex K being strict normal Subgroup of G st

( the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {g} & x = b1 * a1 ) ) )

reconsider H = G as finite strict Subgroup of G by GROUP_2:54;

card H = 1 by AS1, NEWTON:4;

then A1: (1). G = G by GROUP_2:70;

reconsider K = (1). G as strict normal Subgroup of G ;

g in the carrier of ((1). G) by A1;

then g in {(1_ G)} by GROUP_2:def 7;

then A2: g = 1_ G by TARSKI:def 1;

for x being object holds

( x in the carrier of (gr {g}) iff x in {(1_ G)} )

proof

then X1:
the carrier of (gr {g}) = {(1_ G)}
by TARSKI:2;
let x be object ; :: thesis: ( x in the carrier of (gr {g}) iff x in {(1_ G)} )

then x = 1_ G by TARSKI:def 1;

hence x in the carrier of (gr {g}) by GROUP_2:46, STRUCT_0:def 5; :: thesis: verum

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

assume
x in {(1_ G)}
; :: thesis: x in the carrier of (gr {g})assume AA1:
x in the carrier of (gr {g})
; :: thesis: x in {(1_ G)}

then reconsider x0 = x as Element of G by TARSKI:def 3, GROUP_2:def 5;

x0 in gr {g} by AA1;

then consider i being Element of NAT such that

AA2: x0 = g |^ i by GRCY26;

x0 = 1_ G by AA2, A2, GROUP_1:31;

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

end;then reconsider x0 = x as Element of G by TARSKI:def 3, GROUP_2:def 5;

x0 in gr {g} by AA1;

then consider i being Element of NAT such that

AA2: x0 = g |^ i by GRCY26;

x0 = 1_ G by AA2, A2, GROUP_1:31;

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

then x = 1_ G by TARSKI:def 1;

hence x in the carrier of (gr {g}) by GROUP_2:46, STRUCT_0:def 5; :: thesis: verum

the carrier of K = {(1_ G)} by GROUP_2:def 7;

then X2: the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} by X1;

for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {g} & x = b1 * a1 )

proof

hence
ex K being strict normal Subgroup of G st
let x be Element of G; :: thesis: ex b1, a1 being Element of G st

( b1 in K & a1 in gr {g} & x = b1 * a1 )

x in the carrier of ((1). G) by A1;

then x in {(1_ G)} by GROUP_2:def 7;

then x = 1_ G by TARSKI:def 1;

then X3: x = (1_ G) * (1_ G) by GROUP_1:def 4;

( 1_ G in gr {g} & 1_ G in K ) by GROUP_2:46;

hence ex b1, a1 being Element of G st

( b1 in K & a1 in gr {g} & x = b1 * a1 ) by X3; :: thesis: verum

end;( b1 in K & a1 in gr {g} & x = b1 * a1 )

x in the carrier of ((1). G) by A1;

then x in {(1_ G)} by GROUP_2:def 7;

then x = 1_ G by TARSKI:def 1;

then X3: x = (1_ G) * (1_ G) by GROUP_1:def 4;

( 1_ G in gr {g} & 1_ G in K ) by GROUP_2:46;

hence ex b1, a1 being Element of G st

( b1 in K & a1 in gr {g} & x = b1 * a1 ) by X3; :: thesis: verum

( the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {g} & x = b1 * a1 ) ) ) by X2; :: thesis: verum

S

proof

for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume AS1: S_{1}[k]
; :: thesis: S_{1}[k + 1]

let G be finite strict commutative Group; :: thesis: for p being Prime

for g being Element of G st card G = p |^ (k + 1) & ord g = upper_bound (Ordset G) holds

ex K being strict normal Subgroup of G st

( the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {g} & x = b1 * a1 ) ) )

let p be Prime; :: thesis: for g being Element of G st card G = p |^ (k + 1) & ord g = upper_bound (Ordset G) holds

ex K being strict normal Subgroup of G st

( the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {g} & x = b1 * a1 ) ) )

let a be Element of G; :: thesis: ( card G = p |^ (k + 1) & ord a = upper_bound (Ordset G) implies ex K being strict normal Subgroup of G st

( the carrier of K /\ the carrier of (gr {a}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {a} & x = b1 * a1 ) ) ) )

assume A1: ( card G = p |^ (k + 1) & ord a = upper_bound (Ordset G) ) ; :: thesis: ex K being strict normal Subgroup of G st

( the carrier of K /\ the carrier of (gr {a}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {a} & x = b1 * a1 ) ) )

deffunc H_{1}( finite Group) -> Subset of NAT = Ordset $1;

end;assume AS1: S

let G be finite strict commutative Group; :: thesis: for p being Prime

for g being Element of G st card G = p |^ (k + 1) & ord g = upper_bound (Ordset G) holds

ex K being strict normal Subgroup of G st

( the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {g} & x = b1 * a1 ) ) )

let p be Prime; :: thesis: for g being Element of G st card G = p |^ (k + 1) & ord g = upper_bound (Ordset G) holds

ex K being strict normal Subgroup of G st

( the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {g} & x = b1 * a1 ) ) )

let a be Element of G; :: thesis: ( card G = p |^ (k + 1) & ord a = upper_bound (Ordset G) implies ex K being strict normal Subgroup of G st

( the carrier of K /\ the carrier of (gr {a}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {a} & x = b1 * a1 ) ) ) )

assume A1: ( card G = p |^ (k + 1) & ord a = upper_bound (Ordset G) ) ; :: thesis: ex K being strict normal Subgroup of G st

( the carrier of K /\ the carrier of (gr {a}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {a} & x = b1 * a1 ) ) )

deffunc H

per cases
( card (gr {a}) = card G or card (gr {a}) <> card G )
;

end;

suppose CA1:
card (gr {a}) = card G
; :: thesis: ex K being strict normal Subgroup of G st

( the carrier of K /\ the carrier of (gr {a}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {a} & x = b1 * a1 ) ) )

( the carrier of K /\ the carrier of (gr {a}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {a} & x = b1 * a1 ) ) )

then P1:
gr {a} = G
by GROUP_2:73;

reconsider K = (1). G as strict normal Subgroup of G ;

P2: the carrier of K = {(1_ G)} by GROUP_2:def 7;

P3: the carrier of (gr {a}) = the carrier of G by CA1, GROUP_2:73;

X1: the carrier of K /\ the carrier of (gr {a}) = {(1_ G)} by P2, P3, XBOOLE_1:28;

for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {a} & x = b1 * a1 )

( the carrier of K /\ the carrier of (gr {a}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {a} & x = b1 * a1 ) ) ) by X1; :: thesis: verum

end;reconsider K = (1). G as strict normal Subgroup of G ;

P2: the carrier of K = {(1_ G)} by GROUP_2:def 7;

P3: the carrier of (gr {a}) = the carrier of G by CA1, GROUP_2:73;

X1: the carrier of K /\ the carrier of (gr {a}) = {(1_ G)} by P2, P3, XBOOLE_1:28;

for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {a} & x = b1 * a1 )

proof

hence
ex K being strict normal Subgroup of G st
let x be Element of G; :: thesis: ex b1, a1 being Element of G st

( b1 in K & a1 in gr {a} & x = b1 * a1 )

X2: x in gr {a} by P1;

X3: x = (1_ G) * x by GROUP_1:def 4;

1_ G in K by GROUP_2:46;

hence ex b1, a1 being Element of G st

( b1 in K & a1 in gr {a} & x = b1 * a1 ) by X3, X2; :: thesis: verum

end;( b1 in K & a1 in gr {a} & x = b1 * a1 )

X2: x in gr {a} by P1;

X3: x = (1_ G) * x by GROUP_1:def 4;

1_ G in K by GROUP_2:46;

hence ex b1, a1 being Element of G st

( b1 in K & a1 in gr {a} & x = b1 * a1 ) by X3, X2; :: thesis: verum

( the carrier of K /\ the carrier of (gr {a}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {a} & x = b1 * a1 ) ) ) by X1; :: thesis: verum

suppose B2:
card (gr {a}) <> card G
; :: thesis: ex K being strict normal Subgroup of G st

( the carrier of K /\ the carrier of (gr {a}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {a} & x = b1 * a1 ) ) )

( the carrier of K /\ the carrier of (gr {a}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {a} & x = b1 * a1 ) ) )

reconsider Gra = gr {a} as strict normal Subgroup of G by GROUP_3:116;

reconsider G1 = G ./. Gra as finite strict commutative Group by GROUP630;

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

A6: card G = (ord a) * (index Gra) by A5, GROUP_2:147;

consider n1 being Nat such that

A8: ( card Gra = p |^ n1 & n1 <= k + 1 ) by GROUPP_1:2, GROUP_2:148, A1;

(k + 1) - n1 in NAT by A8, XREAL_1:48, INT_1:3;

then reconsider mn1 = (k + 1) - n1 as Nat ;

A9: ord a = p |^ n1 by A8, GR_CY_1:7;

A10: ord a <> 0 by A8, GR_CY_1:7;

A10A: 0 < ord a by A8, GR_CY_1:7;

index Gra = (p |^ (mn1 + n1)) / (p |^ n1) by A6, XCMPLX_1:89, A1, A9

.= ((p |^ mn1) * (p |^ n1)) / (p |^ n1) by NEWTON:8

.= p |^ mn1 by XCMPLX_1:89 ;

then A11: card (G ./. Gra) = p |^ mn1 by GROUP_6:27;

consider b being Element of G such that

A20: not b in Gra by B2, GROUPP_1:12;

reconsider bga = b * Gra as Element of G1 by GROUP_2:def 15;

reconsider Grbga = gr {bga} as strict normal Subgroup of G1 by GROUP_3:116;

consider s being Nat such that

A18: ( card Grbga = p |^ s & s <= mn1 ) by GROUPP_1:2, GROUP_2:148, A11;

A19: ord bga = p |^ s by A18, GR_CY_1:7;

ord bga <> 1

then 0 <= s - 1 by NAT_1:14, XREAL_1:48;

then s - 1 in NAT by INT_1:3;

then reconsider s1 = s - 1 as Nat ;

reconsider c = b |^ (p |^ s1) as Element of G ;

reconsider cga = c * Gra as Element of G1 by GROUP_2:def 15;

A21: (p |^ s1) * p = p |^ (s1 + 1) by NEWTON:6

.= p |^ s ;

XN1: ( p |^ s is Element of NAT & p |^ s1 is Element of NAT & p is Element of NAT ) by ORDINAL1:def 12;

A24: ord (bga |^ (p |^ s1)) = p by XN1, GRCY28, A21, A18;

A23: ord cga = p by A24, GROUPP_1:8;

A26: not c in Gra

A25: cga |^ p = (c |^ p) * Gra by GROUPP_1:8;

(c |^ p) * (1_ G) in (c |^ p) * Gra by GROUP_2:46, GROUP_2:103;

then c |^ p in (c |^ p) * Gra by GROUP_1:def 4;

then c |^ p in gr {a} by A24, A25, GROUP_6:24;

then consider j being Element of NAT such that

A26B: c |^ p = a |^ j by GRCY26;

p divides j

A28: j = p * j1 by NAT_D:def 3;

A28A: j1 is Element of NAT by ORDINAL1:def 12;

set d = c * (a |^ (- j1));

A30: (c * (a |^ (- j1))) |^ p = (c |^ p) * ((a |^ (- j1)) |^ p) by GROUP_1:38

.= (c |^ p) * (a |^ ((- j1) * p)) by GROUP_1:35

.= (c |^ p) * (a |^ (- j)) by A28

.= (c |^ p) * ((a |^ j) ") by GROUP_1:36

.= 1_ G by A26B, GROUP_1:def 5 ;

ord (c * (a |^ (- j1))) <> 1

A33: not c * (a |^ (- j1)) in gr {a}

( x in the carrier of (gr {(c * (a |^ (- j1)))}) /\ the carrier of (gr {a}) iff x in {(1_ G)} )

reconsider Grd = gr {(c * (a |^ (- j1)))} as strict normal Subgroup of G by GROUP_3:116;

reconsider G2 = G ./. Grd as finite strict commutative Group by GROUP630;

D5: ord (c * (a |^ (- j1))) = card (gr {(c * (a |^ (- j1)))}) by GR_CY_1:7;

D6: card G = (ord (c * (a |^ (- j1)))) * (index Grd) by D5, GROUP_2:147;

index Grd = (card G) / (ord (c * (a |^ (- j1)))) by A32, D6, XCMPLX_1:89

.= ((p |^ k) * p) / p by A1, A32, NEWTON:6

.= p |^ k by XCMPLX_1:89 ;

then D11: card (G ./. Grd) = p |^ k by GROUP_6:27;

set Ordset1 = Ordset G2;

set Pd = nat_hom Grd;

D130: nat_hom Grd is onto by GROUP_6:59;

reconsider gd = (nat_hom Grd) . a as Element of G2 ;

set H = (nat_hom Grd) | the carrier of Gra;

D14: (nat_hom Grd) | the carrier of Gra is one-to-one by A3Z, LM204D, TARSKI:2;

D14B: for r being Real st r in Ordset G2 holds

r <= ord gd

ord gd in Ordset G2 ;

then ord gd <= upper_bound (Ordset G2) by SEQ_4:def 1;

then ord gd = upper_bound (Ordset G2) by XXREAL_0:1, XU1;

then consider K2 being strict normal Subgroup of G2 such that

D17: ( the carrier of K2 /\ the carrier of (gr {gd}) = {(1_ G2)} & ( for g2 being Element of G2 ex b2, a2 being Element of G2 st

( b2 in K2 & a2 in gr {gd} & g2 = b2 * a2 ) ) ) by AS1, D11;

consider K being strict Subgroup of G such that

D19: the carrier of K = (nat_hom Grd) " the carrier of K2 by GROUP252INV;

reconsider K = K as strict normal Subgroup of G by GROUP_3:116;

D20: for x being Element of G st x in the carrier of K /\ the carrier of (gr {a}) holds

(nat_hom Grd) . x in the carrier of K2 /\ the carrier of (gr {((nat_hom Grd) . a)})

x in the carrier of (Ker (nat_hom Grd)) /\ the carrier of (gr {a})

then 1_ G in the carrier of K /\ the carrier of (gr {a}) by XBOOLE_0:def 4;

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

for g being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {a} & g = b1 * a1 )

( the carrier of K /\ the carrier of (gr {a}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {a} & x = b1 * a1 ) ) ) by D23A, D23B, XBOOLE_0:def 10; :: thesis: verum

end;reconsider G1 = G ./. Gra as finite strict commutative Group by GROUP630;

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

A6: card G = (ord a) * (index Gra) by A5, GROUP_2:147;

consider n1 being Nat such that

A8: ( card Gra = p |^ n1 & n1 <= k + 1 ) by GROUPP_1:2, GROUP_2:148, A1;

(k + 1) - n1 in NAT by A8, XREAL_1:48, INT_1:3;

then reconsider mn1 = (k + 1) - n1 as Nat ;

A9: ord a = p |^ n1 by A8, GR_CY_1:7;

A10: ord a <> 0 by A8, GR_CY_1:7;

A10A: 0 < ord a by A8, GR_CY_1:7;

index Gra = (p |^ (mn1 + n1)) / (p |^ n1) by A6, XCMPLX_1:89, A1, A9

.= ((p |^ mn1) * (p |^ n1)) / (p |^ n1) by NEWTON:8

.= p |^ mn1 by XCMPLX_1:89 ;

then A11: card (G ./. Gra) = p |^ mn1 by GROUP_6:27;

consider b being Element of G such that

A20: not b in Gra by B2, GROUPP_1:12;

reconsider bga = b * Gra as Element of G1 by GROUP_2:def 15;

reconsider Grbga = gr {bga} as strict normal Subgroup of G1 by GROUP_3:116;

consider s being Nat such that

A18: ( card Grbga = p |^ s & s <= mn1 ) by GROUPP_1:2, GROUP_2:148, A11;

A19: ord bga = p |^ s by A18, GR_CY_1:7;

ord bga <> 1

proof

then
s <> 0
by A19, NEWTON:4;
assume
ord bga = 1
; :: thesis: contradiction

then bga = 1_ G1 by GROUP_1:43;

then A191: b * Gra = the carrier of Gra by GROUP_6:24;

b * (1_ G) in b * Gra by GROUP_2:46, GROUP_2:103;

hence contradiction by A20, A191, GROUP_1:def 4; :: thesis: verum

end;then bga = 1_ G1 by GROUP_1:43;

then A191: b * Gra = the carrier of Gra by GROUP_6:24;

b * (1_ G) in b * Gra by GROUP_2:46, GROUP_2:103;

hence contradiction by A20, A191, GROUP_1:def 4; :: thesis: verum

then 0 <= s - 1 by NAT_1:14, XREAL_1:48;

then s - 1 in NAT by INT_1:3;

then reconsider s1 = s - 1 as Nat ;

reconsider c = b |^ (p |^ s1) as Element of G ;

reconsider cga = c * Gra as Element of G1 by GROUP_2:def 15;

A21: (p |^ s1) * p = p |^ (s1 + 1) by NEWTON:6

.= p |^ s ;

XN1: ( p |^ s is Element of NAT & p |^ s1 is Element of NAT & p is Element of NAT ) by ORDINAL1:def 12;

A24: ord (bga |^ (p |^ s1)) = p by XN1, GRCY28, A21, A18;

A23: ord cga = p by A24, GROUPP_1:8;

A26: not c in Gra

proof

A24:
cga |^ p = 1_ G1
by A23, GROUP_1:41;
assume A261:
c in Gra
; :: thesis: contradiction

cga = carr Gra by A261, GROUP_2:113

.= 1_ G1 by GROUP_6:24 ;

then ord cga = 1 by GROUP_1:42;

hence contradiction by A23, INT_2:def 4; :: thesis: verum

end;cga = carr Gra by A261, GROUP_2:113

.= 1_ G1 by GROUP_6:24 ;

then ord cga = 1 by GROUP_1:42;

hence contradiction by A23, INT_2:def 4; :: thesis: verum

A25: cga |^ p = (c |^ p) * Gra by GROUPP_1:8;

(c |^ p) * (1_ G) in (c |^ p) * Gra by GROUP_2:46, GROUP_2:103;

then c |^ p in (c |^ p) * Gra by GROUP_1:def 4;

then c |^ p in gr {a} by A24, A25, GROUP_6:24;

then consider j being Element of NAT such that

A26B: c |^ p = a |^ j by GRCY26;

p divides j

proof

then consider j1 being Nat such that
assume
not p divides j
; :: thesis: contradiction

then A27Z: j gcd (ord a) = 1 by A8, LM204K, GR_CY_1:7;

A272: ord (c |^ p) = ord a by A26B, A27Z, GRCY212A;

A273: ord c = p * (ord (c |^ p))

ord c in Ordset G ;

hence contradiction by XXX0, A1, A272, A273, SEQ_4:def 1; :: thesis: verum

end;then A27Z: j gcd (ord a) = 1 by A8, LM204K, GR_CY_1:7;

A272: ord (c |^ p) = ord a by A26B, A27Z, GRCY212A;

A273: ord c = p * (ord (c |^ p))

proof

XXX0:
1 * (ord a) < p * (ord a)
by A10A, XREAL_1:68, INT_2:def 4;
ord (c |^ p) <> 0
by A10, A26B, A27Z, GRCY212A;

then A274: ord c <= p * (ord (c |^ p)) by XN1, GRCY211, NAT_D:7;

c <> 1_ G by A26, GROUP_2:46;

then consider k being Nat such that

A2750: ord c = p |^ (k + 1) by A1, LM204I;

A275B: p * (p |^ k) = ord c by A2750, NEWTON:6;

A275: (ord c) / p = p |^ k by A275B, XCMPLX_1:89;

(c |^ p) |^ (p |^ k) = c |^ (p * (p |^ k)) by GROUP_1:35

.= 1_ G by A275B, GROUP_1:41 ;

then ord (c |^ p) <= (ord c) / p by A275, NAT_D:7, GROUP_1:44;

then p * (ord (c |^ p)) <= ord c by XREAL_1:83;

hence ord c = p * (ord (c |^ p)) by A274, XXREAL_0:1; :: thesis: verum

end;then A274: ord c <= p * (ord (c |^ p)) by XN1, GRCY211, NAT_D:7;

c <> 1_ G by A26, GROUP_2:46;

then consider k being Nat such that

A2750: ord c = p |^ (k + 1) by A1, LM204I;

A275B: p * (p |^ k) = ord c by A2750, NEWTON:6;

A275: (ord c) / p = p |^ k by A275B, XCMPLX_1:89;

(c |^ p) |^ (p |^ k) = c |^ (p * (p |^ k)) by GROUP_1:35

.= 1_ G by A275B, GROUP_1:41 ;

then ord (c |^ p) <= (ord c) / p by A275, NAT_D:7, GROUP_1:44;

then p * (ord (c |^ p)) <= ord c by XREAL_1:83;

hence ord c = p * (ord (c |^ p)) by A274, XXREAL_0:1; :: thesis: verum

ord c in Ordset G ;

hence contradiction by XXX0, A1, A272, A273, SEQ_4:def 1; :: thesis: verum

A28: j = p * j1 by NAT_D:def 3;

A28A: j1 is Element of NAT by ORDINAL1:def 12;

set d = c * (a |^ (- j1));

A30: (c * (a |^ (- j1))) |^ p = (c |^ p) * ((a |^ (- j1)) |^ p) by GROUP_1:38

.= (c |^ p) * (a |^ ((- j1) * p)) by GROUP_1:35

.= (c |^ p) * (a |^ (- j)) by A28

.= (c |^ p) * ((a |^ j) ") by GROUP_1:36

.= 1_ G by A26B, GROUP_1:def 5 ;

ord (c * (a |^ (- j1))) <> 1

proof

then A32:
ord (c * (a |^ (- j1))) = p
by A30, INT_2:def 4, GROUP_1:44;
assume
ord (c * (a |^ (- j1))) = 1
; :: thesis: contradiction

then c * (a |^ (- j1)) = 1_ G by GROUP_1:43;

then c " = a |^ (- j1) by GROUP_1:12;

then c " = (a |^ j1) " by GROUP_1:36;

hence contradiction by A26, A28A, GRCY26, GROUP_1:9; :: thesis: verum

end;then c * (a |^ (- j1)) = 1_ G by GROUP_1:43;

then c " = a |^ (- j1) by GROUP_1:12;

then c " = (a |^ j1) " by GROUP_1:36;

hence contradiction by A26, A28A, GRCY26, GROUP_1:9; :: thesis: verum

A33: not c * (a |^ (- j1)) in gr {a}

proof

A3Z:
for x being object holds
assume
c * (a |^ (- j1)) in gr {a}
; :: thesis: contradiction

then consider k being Element of NAT such that

A331: c * (a |^ (- j1)) = a |^ k by GRCY26;

c * ((a |^ j1) ") = a |^ k by GROUP_1:36, A331;

then c = (a |^ k) * (a |^ j1) by GROUP_1:14;

then c = a |^ (j1 + k) by GROUP_1:33;

hence contradiction by A26, GRCY26; :: thesis: verum

end;then consider k being Element of NAT such that

A331: c * (a |^ (- j1)) = a |^ k by GRCY26;

c * ((a |^ j1) ") = a |^ k by GROUP_1:36, A331;

then c = (a |^ k) * (a |^ j1) by GROUP_1:14;

then c = a |^ (j1 + k) by GROUP_1:33;

hence contradiction by A26, GRCY26; :: thesis: verum

( x in the carrier of (gr {(c * (a |^ (- j1)))}) /\ the carrier of (gr {a}) iff x in {(1_ G)} )

proof

then A33:
the carrier of (gr {(c * (a |^ (- j1)))}) /\ the carrier of (gr {a}) = {(1_ G)}
by TARSKI:2;
let x0 be object ; :: thesis: ( x0 in the carrier of (gr {(c * (a |^ (- j1)))}) /\ the carrier of (gr {a}) iff x0 in {(1_ G)} )

then x0 = 1_ G by TARSKI:def 1;

then ( x0 in the carrier of (gr {(c * (a |^ (- j1)))}) & x0 in the carrier of (gr {a}) ) by GROUP_2:46, STRUCT_0:def 5;

hence x0 in the carrier of (gr {(c * (a |^ (- j1)))}) /\ the carrier of (gr {a}) by XBOOLE_0:def 4; :: thesis: verum

end;hereby :: thesis: ( x0 in {(1_ G)} implies x0 in the carrier of (gr {(c * (a |^ (- j1)))}) /\ the carrier of (gr {a}) )

assume
x0 in {(1_ G)}
; :: thesis: x0 in the carrier of (gr {(c * (a |^ (- j1)))}) /\ the carrier of (gr {a})assume A310:
x0 in the carrier of (gr {(c * (a |^ (- j1)))}) /\ the carrier of (gr {a})
; :: thesis: x0 in {(1_ G)}

then ( x0 in the carrier of (gr {(c * (a |^ (- j1)))}) & x0 in the carrier of (gr {a}) ) by XBOOLE_0:def 4;

then reconsider x = x0 as Element of G by GROUP_2:def 5, TARSKI:def 3;

x in gr {(c * (a |^ (- j1)))} by A310, XBOOLE_0:def 4;

then A322: ( x = 1_ G or gr {x} = gr {(c * (a |^ (- j1)))} ) by GRCY112, A32;

x in gr {a} by A310, XBOOLE_0:def 4;

then X1: gr {x} is strict Subgroup of gr {a} by GRCY212;

gr {x} <> gr {(c * (a |^ (- j1)))}

end;then ( x0 in the carrier of (gr {(c * (a |^ (- j1)))}) & x0 in the carrier of (gr {a}) ) by XBOOLE_0:def 4;

then reconsider x = x0 as Element of G by GROUP_2:def 5, TARSKI:def 3;

x in gr {(c * (a |^ (- j1)))} by A310, XBOOLE_0:def 4;

then A322: ( x = 1_ G or gr {x} = gr {(c * (a |^ (- j1)))} ) by GRCY112, A32;

x in gr {a} by A310, XBOOLE_0:def 4;

then X1: gr {x} is strict Subgroup of gr {a} by GRCY212;

gr {x} <> gr {(c * (a |^ (- j1)))}

proof

hence
x0 in {(1_ G)}
by A322, TARSKI:def 1; :: thesis: verum
assume
gr {x} = gr {(c * (a |^ (- j1)))}
; :: thesis: contradiction

then XX1: the carrier of (gr {(c * (a |^ (- j1)))}) c= the carrier of (gr {a}) by X1, GROUP_2:def 5;

c * (a |^ (- j1)) in gr {(c * (a |^ (- j1)))} by GR_CY_2:2;

hence contradiction by A33, XX1; :: thesis: verum

end;then XX1: the carrier of (gr {(c * (a |^ (- j1)))}) c= the carrier of (gr {a}) by X1, GROUP_2:def 5;

c * (a |^ (- j1)) in gr {(c * (a |^ (- j1)))} by GR_CY_2:2;

hence contradiction by A33, XX1; :: thesis: verum

then x0 = 1_ G by TARSKI:def 1;

then ( x0 in the carrier of (gr {(c * (a |^ (- j1)))}) & x0 in the carrier of (gr {a}) ) by GROUP_2:46, STRUCT_0:def 5;

hence x0 in the carrier of (gr {(c * (a |^ (- j1)))}) /\ the carrier of (gr {a}) by XBOOLE_0:def 4; :: thesis: verum

reconsider Grd = gr {(c * (a |^ (- j1)))} as strict normal Subgroup of G by GROUP_3:116;

reconsider G2 = G ./. Grd as finite strict commutative Group by GROUP630;

D5: ord (c * (a |^ (- j1))) = card (gr {(c * (a |^ (- j1)))}) by GR_CY_1:7;

D6: card G = (ord (c * (a |^ (- j1)))) * (index Grd) by D5, GROUP_2:147;

index Grd = (card G) / (ord (c * (a |^ (- j1)))) by A32, D6, XCMPLX_1:89

.= ((p |^ k) * p) / p by A1, A32, NEWTON:6

.= p |^ k by XCMPLX_1:89 ;

then D11: card (G ./. Grd) = p |^ k by GROUP_6:27;

set Ordset1 = Ordset G2;

set Pd = nat_hom Grd;

D130: nat_hom Grd is onto by GROUP_6:59;

reconsider gd = (nat_hom Grd) . a as Element of G2 ;

set H = (nat_hom Grd) | the carrier of Gra;

D14: (nat_hom Grd) | the carrier of Gra is one-to-one by A3Z, LM204D, TARSKI:2;

D14B: for r being Real st r in Ordset G2 holds

r <= ord gd

proof

XU1:
upper_bound (Ordset G2) <= ord gd
by SEQ_4:45, D14B;
assume
ex r being Real st

( r in Ordset G2 & not r <= ord gd ) ; :: thesis: contradiction

then consider r being Real such that

D141: ( r in Ordset G2 & not r <= ord gd ) ;

D142: ord a < r by D141, D14, LM204H;

consider gx being Element of G2 such that

D143: r = ord gx by D141;

rng (nat_hom Grd) = the carrier of G2 by D130, FUNCT_2:def 3;

then consider a1 being Element of G such that

D232: gx = (nat_hom Grd) . a1 by FUNCT_2:113;

ord gx <= ord a1 by D232, LM204E;

then X1: ord a < ord a1 by XXREAL_0:2, D143, D142;

ord a1 in Ordset G ;

hence contradiction by X1, A1, SEQ_4:def 1; :: thesis: verum

end;( r in Ordset G2 & not r <= ord gd ) ; :: thesis: contradiction

then consider r being Real such that

D141: ( r in Ordset G2 & not r <= ord gd ) ;

D142: ord a < r by D141, D14, LM204H;

consider gx being Element of G2 such that

D143: r = ord gx by D141;

rng (nat_hom Grd) = the carrier of G2 by D130, FUNCT_2:def 3;

then consider a1 being Element of G such that

D232: gx = (nat_hom Grd) . a1 by FUNCT_2:113;

ord gx <= ord a1 by D232, LM204E;

then X1: ord a < ord a1 by XXREAL_0:2, D143, D142;

ord a1 in Ordset G ;

hence contradiction by X1, A1, SEQ_4:def 1; :: thesis: verum

ord gd in Ordset G2 ;

then ord gd <= upper_bound (Ordset G2) by SEQ_4:def 1;

then ord gd = upper_bound (Ordset G2) by XXREAL_0:1, XU1;

then consider K2 being strict normal Subgroup of G2 such that

D17: ( the carrier of K2 /\ the carrier of (gr {gd}) = {(1_ G2)} & ( for g2 being Element of G2 ex b2, a2 being Element of G2 st

( b2 in K2 & a2 in gr {gd} & g2 = b2 * a2 ) ) ) by AS1, D11;

consider K being strict Subgroup of G such that

D19: the carrier of K = (nat_hom Grd) " the carrier of K2 by GROUP252INV;

reconsider K = K as strict normal Subgroup of G by GROUP_3:116;

D20: for x being Element of G st x in the carrier of K /\ the carrier of (gr {a}) holds

(nat_hom Grd) . x in the carrier of K2 /\ the carrier of (gr {((nat_hom Grd) . a)})

proof

D22:
for x being Element of G st x in the carrier of K /\ the carrier of (gr {a}) holds
let x be Element of G; :: thesis: ( x in the carrier of K /\ the carrier of (gr {a}) implies (nat_hom Grd) . x in the carrier of K2 /\ the carrier of (gr {((nat_hom Grd) . a)}) )

assume D20A: x in the carrier of K /\ the carrier of (gr {a}) ; :: thesis: (nat_hom Grd) . x in the carrier of K2 /\ the carrier of (gr {((nat_hom Grd) . a)})

then D20B: ( x in the carrier of (gr {a}) & x in the carrier of K ) by XBOOLE_0:def 4;

x in gr {a} by D20A, XBOOLE_0:def 4;

then consider k being Element of NAT such that

D20C: x = a |^ k by GRCY26;

XXX: (nat_hom Grd) . x is Element of G2 ;

(nat_hom Grd) . x = ((nat_hom Grd) . a) |^ k by D20C, GROUP_6:37;

then D233: (nat_hom Grd) . x in gr {((nat_hom Grd) . a)} by XXX, GRCY26;

(nat_hom Grd) . x in the carrier of K2 by D20B, D19, FUNCT_2:38;

hence (nat_hom Grd) . x in the carrier of K2 /\ the carrier of (gr {((nat_hom Grd) . a)}) by D233, XBOOLE_0:def 4; :: thesis: verum

end;assume D20A: x in the carrier of K /\ the carrier of (gr {a}) ; :: thesis: (nat_hom Grd) . x in the carrier of K2 /\ the carrier of (gr {((nat_hom Grd) . a)})

then D20B: ( x in the carrier of (gr {a}) & x in the carrier of K ) by XBOOLE_0:def 4;

x in gr {a} by D20A, XBOOLE_0:def 4;

then consider k being Element of NAT such that

D20C: x = a |^ k by GRCY26;

XXX: (nat_hom Grd) . x is Element of G2 ;

(nat_hom Grd) . x = ((nat_hom Grd) . a) |^ k by D20C, GROUP_6:37;

then D233: (nat_hom Grd) . x in gr {((nat_hom Grd) . a)} by XXX, GRCY26;

(nat_hom Grd) . x in the carrier of K2 by D20B, D19, FUNCT_2:38;

hence (nat_hom Grd) . x in the carrier of K2 /\ the carrier of (gr {((nat_hom Grd) . a)}) by D233, XBOOLE_0:def 4; :: thesis: verum

x in the carrier of (Ker (nat_hom Grd)) /\ the carrier of (gr {a})

proof

D23A:
the carrier of K /\ the carrier of (gr {a}) c= {(1_ G)}
let x be Element of G; :: thesis: ( x in the carrier of K /\ the carrier of (gr {a}) implies x in the carrier of (Ker (nat_hom Grd)) /\ the carrier of (gr {a}) )

assume D22A: x in the carrier of K /\ the carrier of (gr {a}) ; :: thesis: x in the carrier of (Ker (nat_hom Grd)) /\ the carrier of (gr {a})

then (nat_hom Grd) . x in {(1_ G2)} by D17, D20;

then (nat_hom Grd) . x = 1_ G2 by TARSKI:def 1;

then x in { s where s is Element of G : (nat_hom Grd) . s = 1_ G2 } ;

then D22B: x in the carrier of (Ker (nat_hom Grd)) by GROUP_6:def 9;

x in the carrier of (gr {a}) by D22A, XBOOLE_0:def 4;

hence x in the carrier of (Ker (nat_hom Grd)) /\ the carrier of (gr {a}) by D22B, XBOOLE_0:def 4; :: thesis: verum

end;assume D22A: x in the carrier of K /\ the carrier of (gr {a}) ; :: thesis: x in the carrier of (Ker (nat_hom Grd)) /\ the carrier of (gr {a})

then (nat_hom Grd) . x in {(1_ G2)} by D17, D20;

then (nat_hom Grd) . x = 1_ G2 by TARSKI:def 1;

then x in { s where s is Element of G : (nat_hom Grd) . s = 1_ G2 } ;

then D22B: x in the carrier of (Ker (nat_hom Grd)) by GROUP_6:def 9;

x in the carrier of (gr {a}) by D22A, XBOOLE_0:def 4;

hence x in the carrier of (Ker (nat_hom Grd)) /\ the carrier of (gr {a}) by D22B, XBOOLE_0:def 4; :: thesis: verum

proof

( 1_ G in the carrier of (gr {a}) & 1_ G in the carrier of K )
by STRUCT_0:def 5, GROUP_2:46;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of K /\ the carrier of (gr {a}) or x in {(1_ G)} )

assume D221: x in the carrier of K /\ the carrier of (gr {a}) ; :: thesis: x in {(1_ G)}

then x in the carrier of K by XBOOLE_0:def 4;

then reconsider x0 = x as Element of G by TARSKI:def 3, GROUP_2:def 5;

x0 in the carrier of (Ker (nat_hom Grd)) /\ the carrier of (gr {a}) by D22, D221;

then D222: ( x0 in the carrier of (gr {a}) & x0 in the carrier of (Ker (nat_hom Grd)) ) by XBOOLE_0:def 4;

then x0 in the carrier of (gr {(c * (a |^ (- j1)))}) by GROUP_6:43;

hence x in {(1_ G)} by A33, D222, XBOOLE_0:def 4; :: thesis: verum

end;assume D221: x in the carrier of K /\ the carrier of (gr {a}) ; :: thesis: x in {(1_ G)}

then x in the carrier of K by XBOOLE_0:def 4;

then reconsider x0 = x as Element of G by TARSKI:def 3, GROUP_2:def 5;

x0 in the carrier of (Ker (nat_hom Grd)) /\ the carrier of (gr {a}) by D22, D221;

then D222: ( x0 in the carrier of (gr {a}) & x0 in the carrier of (Ker (nat_hom Grd)) ) by XBOOLE_0:def 4;

then x0 in the carrier of (gr {(c * (a |^ (- j1)))}) by GROUP_6:43;

hence x in {(1_ G)} by A33, D222, XBOOLE_0:def 4; :: thesis: verum

then 1_ G in the carrier of K /\ the carrier of (gr {a}) by XBOOLE_0:def 4;

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

for g being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {a} & g = b1 * a1 )

proof

hence
ex K being strict normal Subgroup of G st
let g be Element of G; :: thesis: ex b1, a1 being Element of G st

( b1 in K & a1 in gr {a} & g = b1 * a1 )

reconsider g2 = (nat_hom Grd) . g as Element of G2 ;

consider b2, a2 being Element of G2 such that

D231: ( b2 in K2 & a2 in gr {gd} & g2 = b2 * a2 ) by D17;

consider i being Element of NAT such that

D231A: a2 = gd |^ i by GRCY26, D231;

rng (nat_hom Grd) = the carrier of G2 by D130, FUNCT_2:def 3;

then consider b1 being Element of the carrier of G such that

D232: b2 = (nat_hom Grd) . b1 by FUNCT_2:113;

D234: (nat_hom Grd) . ((a |^ i) * b1) = ((nat_hom Grd) . (a |^ i)) * ((nat_hom Grd) . b1) by GROUP_6:def 6

.= (nat_hom Grd) . g by D231A, D231, D232, GROUP_6:37 ;

D235: ((a |^ i) * b1) * (gr {(c * (a |^ (- j1)))}) = (nat_hom Grd) . ((a |^ i) * b1) by GROUP_6:def 8

.= g * (gr {(c * (a |^ (- j1)))}) by D234, GROUP_6:def 8 ;

g * (1_ G) in g * (gr {(c * (a |^ (- j1)))}) by GROUP_2:46, GROUP_2:103;

then g in ((a |^ i) * b1) * (gr {(c * (a |^ (- j1)))}) by D235, GROUP_1:def 4;

then consider y being Element of G such that

D236: ( g = ((a |^ i) * b1) * y & y in gr {(c * (a |^ (- j1)))} ) by GROUP_2:103;

D236A: g = (a |^ i) * (b1 * y) by D236, GROUP_1:def 3;

consider j being Element of NAT such that

D237: y = (c * (a |^ (- j1))) |^ j by GRCY26, D236;

D238: (nat_hom Grd) . (c * (a |^ (- j1))) = (c * (a |^ (- j1))) * (gr {(c * (a |^ (- j1)))}) by GROUP_6:def 8

.= carr (gr {(c * (a |^ (- j1)))}) by GR_CY_2:2, GROUP_2:113

.= 1_ G2 by GROUP_6:24 ;

D239: (nat_hom Grd) . y = ((nat_hom Grd) . (c * (a |^ (- j1)))) |^ j by D237, GROUP_6:37

.= 1_ G2 by D238, GROUP_1:31 ;

1_ G2 in the carrier of K2 by GROUP_2:46, STRUCT_0:def 5;

then ( b1 in K & y in K ) by D19, D231, D232, D239, FUNCT_2:38;

then b1 * y in K by GROUP_2:50;

hence ex b1, a1 being Element of G st

( b1 in K & a1 in gr {a} & g = b1 * a1 ) by D236A, GRCY26; :: thesis: verum

end;( b1 in K & a1 in gr {a} & g = b1 * a1 )

reconsider g2 = (nat_hom Grd) . g as Element of G2 ;

consider b2, a2 being Element of G2 such that

D231: ( b2 in K2 & a2 in gr {gd} & g2 = b2 * a2 ) by D17;

consider i being Element of NAT such that

D231A: a2 = gd |^ i by GRCY26, D231;

rng (nat_hom Grd) = the carrier of G2 by D130, FUNCT_2:def 3;

then consider b1 being Element of the carrier of G such that

D232: b2 = (nat_hom Grd) . b1 by FUNCT_2:113;

D234: (nat_hom Grd) . ((a |^ i) * b1) = ((nat_hom Grd) . (a |^ i)) * ((nat_hom Grd) . b1) by GROUP_6:def 6

.= (nat_hom Grd) . g by D231A, D231, D232, GROUP_6:37 ;

D235: ((a |^ i) * b1) * (gr {(c * (a |^ (- j1)))}) = (nat_hom Grd) . ((a |^ i) * b1) by GROUP_6:def 8

.= g * (gr {(c * (a |^ (- j1)))}) by D234, GROUP_6:def 8 ;

g * (1_ G) in g * (gr {(c * (a |^ (- j1)))}) by GROUP_2:46, GROUP_2:103;

then g in ((a |^ i) * b1) * (gr {(c * (a |^ (- j1)))}) by D235, GROUP_1:def 4;

then consider y being Element of G such that

D236: ( g = ((a |^ i) * b1) * y & y in gr {(c * (a |^ (- j1)))} ) by GROUP_2:103;

D236A: g = (a |^ i) * (b1 * y) by D236, GROUP_1:def 3;

consider j being Element of NAT such that

D237: y = (c * (a |^ (- j1))) |^ j by GRCY26, D236;

D238: (nat_hom Grd) . (c * (a |^ (- j1))) = (c * (a |^ (- j1))) * (gr {(c * (a |^ (- j1)))}) by GROUP_6:def 8

.= carr (gr {(c * (a |^ (- j1)))}) by GR_CY_2:2, GROUP_2:113

.= 1_ G2 by GROUP_6:24 ;

D239: (nat_hom Grd) . y = ((nat_hom Grd) . (c * (a |^ (- j1)))) |^ j by D237, GROUP_6:37

.= 1_ G2 by D238, GROUP_1:31 ;

1_ G2 in the carrier of K2 by GROUP_2:46, STRUCT_0:def 5;

then ( b1 in K & y in K ) by D19, D231, D232, D239, FUNCT_2:38;

then b1 * y in K by GROUP_2:50;

hence ex b1, a1 being Element of G st

( b1 in K & a1 in gr {a} & g = b1 * a1 ) by D236A, GRCY26; :: thesis: verum

( the carrier of K /\ the carrier of (gr {a}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {a} & x = b1 * a1 ) ) ) by D23A, D23B, XBOOLE_0:def 10; :: thesis: verum

hence for G being finite strict commutative Group

for p being Prime

for m being Nat

for g being Element of G st card G = p |^ m & ord g = upper_bound (Ordset G) holds

ex K being strict normal Subgroup of G st

( the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st

( b1 in K & a1 in gr {g} & x = b1 * a1 ) ) ) ; :: thesis: verum