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

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

ex K being strict normal Subgroup of G ex n, k being Nat ex g being Element of G st

( ord g = upper_bound (Ordset G) & K is finite & K is commutative & 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 ) ) & ord g = p |^ n & k = m - n & n <= m & card K = p |^ k & ex F being Homomorphism of (product <*K,(gr {g})*>),G st

( F is bijective & ( for a, b being Element of G st a in K & b in gr {g} holds

F . <*a,b*> = a * b ) ) )

let p be Prime; :: thesis: for m being Nat st card G = p |^ m holds

ex K being strict normal Subgroup of G ex n, k being Nat ex g being Element of G st

( ord g = upper_bound (Ordset G) & K is finite & K is commutative & 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 ) ) & ord g = p |^ n & k = m - n & n <= m & card K = p |^ k & ex F being Homomorphism of (product <*K,(gr {g})*>),G st

( F is bijective & ( for a, b being Element of G st a in K & b in gr {g} holds

F . <*a,b*> = a * b ) ) )

let m be Nat; :: thesis: ( card G = p |^ m implies ex K being strict normal Subgroup of G ex n, k being Nat ex g being Element of G st

( ord g = upper_bound (Ordset G) & K is finite & K is commutative & 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 ) ) & ord g = p |^ n & k = m - n & n <= m & card K = p |^ k & ex F being Homomorphism of (product <*K,(gr {g})*>),G st

( F is bijective & ( for a, b being Element of G st a in K & b in gr {g} holds

F . <*a,b*> = a * b ) ) ) )

assume AS: card G = p |^ m ; :: thesis: ex K being strict normal Subgroup of G ex n, k being Nat ex g being Element of G st

( ord g = upper_bound (Ordset G) & K is finite & K is commutative & 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 ) ) & ord g = p |^ n & k = m - n & n <= m & card K = p |^ k & ex F being Homomorphism of (product <*K,(gr {g})*>),G st

( F is bijective & ( for a, b being Element of G st a in K & b in gr {g} holds

F . <*a,b*> = a * b ) ) )

consider g being Element of G such that

A0: ord g = upper_bound (Ordset G) by LM202;

consider K being strict normal Subgroup of G such that

P1: ( 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 AS, A0, LM204A;

consider n being Nat such that

Q4: ( card (gr {g}) = p |^ n & n <= m ) by AS, GROUPP_1:2, GROUP_2:148;

m - n in NAT by Q4, INT_1:3, XREAL_1:48;

then reconsider k = m - n as Nat ;

gr {g} is normal Subgroup of G by GROUP_3:116;

then consider F being Homomorphism of (product <*K,(gr {g})*>),G such that

P5: ( F is bijective & ( for a, b being Element of G st a in K & b in gr {g} holds

F . <*a,b*> = a * b ) ) by P1, GROUP_17:12;

set s = card K;

set t = card (gr {g});

( F is one-to-one & dom F = the carrier of (product <*K,(gr {g})*>) & rng F = the carrier of G ) by P5, FUNCT_2:def 1, FUNCT_2:def 3;

then X6: card (product <*K,(gr {g})*>) = card G by CARD_1:5, WELLORD2:def 4;

(card K) * (p |^ n) = p |^ (k + n) by X6, Q4, AS, GROUP_17:17

.= (p |^ k) * (p |^ n) by NEWTON:8 ;

then card K = p |^ k by XCMPLX_1:5;

hence ex K being strict normal Subgroup of G ex n, k being Nat ex g being Element of G st

( ord g = upper_bound (Ordset G) & K is finite & K is commutative & 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 ) ) & ord g = p |^ n & k = m - n & n <= m & card K = p |^ k & ex F being Homomorphism of (product <*K,(gr {g})*>),G st

( F is bijective & ( for a, b being Element of G st a in K & b in gr {g} holds

F . <*a,b*> = a * b ) ) ) by A0, P1, P5, Q4, GR_CY_1:7; :: thesis: verum

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

ex K being strict normal Subgroup of G ex n, k being Nat ex g being Element of G st

( ord g = upper_bound (Ordset G) & K is finite & K is commutative & 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 ) ) & ord g = p |^ n & k = m - n & n <= m & card K = p |^ k & ex F being Homomorphism of (product <*K,(gr {g})*>),G st

( F is bijective & ( for a, b being Element of G st a in K & b in gr {g} holds

F . <*a,b*> = a * b ) ) )

let p be Prime; :: thesis: for m being Nat st card G = p |^ m holds

ex K being strict normal Subgroup of G ex n, k being Nat ex g being Element of G st

( ord g = upper_bound (Ordset G) & K is finite & K is commutative & 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 ) ) & ord g = p |^ n & k = m - n & n <= m & card K = p |^ k & ex F being Homomorphism of (product <*K,(gr {g})*>),G st

( F is bijective & ( for a, b being Element of G st a in K & b in gr {g} holds

F . <*a,b*> = a * b ) ) )

let m be Nat; :: thesis: ( card G = p |^ m implies ex K being strict normal Subgroup of G ex n, k being Nat ex g being Element of G st

( ord g = upper_bound (Ordset G) & K is finite & K is commutative & 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 ) ) & ord g = p |^ n & k = m - n & n <= m & card K = p |^ k & ex F being Homomorphism of (product <*K,(gr {g})*>),G st

( F is bijective & ( for a, b being Element of G st a in K & b in gr {g} holds

F . <*a,b*> = a * b ) ) ) )

assume AS: card G = p |^ m ; :: thesis: ex K being strict normal Subgroup of G ex n, k being Nat ex g being Element of G st

( ord g = upper_bound (Ordset G) & K is finite & K is commutative & 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 ) ) & ord g = p |^ n & k = m - n & n <= m & card K = p |^ k & ex F being Homomorphism of (product <*K,(gr {g})*>),G st

( F is bijective & ( for a, b being Element of G st a in K & b in gr {g} holds

F . <*a,b*> = a * b ) ) )

consider g being Element of G such that

A0: ord g = upper_bound (Ordset G) by LM202;

consider K being strict normal Subgroup of G such that

P1: ( 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 AS, A0, LM204A;

consider n being Nat such that

Q4: ( card (gr {g}) = p |^ n & n <= m ) by AS, GROUPP_1:2, GROUP_2:148;

m - n in NAT by Q4, INT_1:3, XREAL_1:48;

then reconsider k = m - n as Nat ;

gr {g} is normal Subgroup of G by GROUP_3:116;

then consider F being Homomorphism of (product <*K,(gr {g})*>),G such that

P5: ( F is bijective & ( for a, b being Element of G st a in K & b in gr {g} holds

F . <*a,b*> = a * b ) ) by P1, GROUP_17:12;

set s = card K;

set t = card (gr {g});

( F is one-to-one & dom F = the carrier of (product <*K,(gr {g})*>) & rng F = the carrier of G ) by P5, FUNCT_2:def 1, FUNCT_2:def 3;

then X6: card (product <*K,(gr {g})*>) = card G by CARD_1:5, WELLORD2:def 4;

(card K) * (p |^ n) = p |^ (k + n) by X6, Q4, AS, GROUP_17:17

.= (p |^ k) * (p |^ n) by NEWTON:8 ;

then card K = p |^ k by XCMPLX_1:5;

hence ex K being strict normal Subgroup of G ex n, k being Nat ex g being Element of G st

( ord g = upper_bound (Ordset G) & K is finite & K is commutative & 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 ) ) & ord g = p |^ n & k = m - n & n <= m & card K = p |^ k & ex F being Homomorphism of (product <*K,(gr {g})*>),G st

( F is bijective & ( for a, b being Element of G st a in K & b in gr {g} holds

F . <*a,b*> = a * b ) ) ) by A0, P1, P5, Q4, GR_CY_1:7; :: thesis: verum