reconsider x1 = 1, x2 = 0 as set ;
let G be finite Group; :: thesis: for p being Prime ex P being strict Subgroup of G st P is_Sylow_p-subgroup_of_prime p
let p be Prime; :: thesis: ex P being strict Subgroup of G st P is_Sylow_p-subgroup_of_prime p
reconsider p9 = p as prime Element of NAT by ORDINAL1:def 12;
set n = card G;
set LO = the_left_operation_of G;
consider m, r being Nat such that
A1: card G = (p |^ r) * m and
A2: not p divides m by Lm2;
reconsider k1 = p9 |^ r as Element of NAT by ORDINAL1:def 12;
set SF = the_subsets_of_card (k1, the carrier of G);
card (the_subsets_of_card (k1, the carrier of G)) = card (Choose ( the carrier of G,k1,x1,x2)) by Th2;
then A3: card (the_subsets_of_card (k1, the carrier of G)) = (card G) choose k1 by CARD_FIN:16;
then (card (the_subsets_of_card (k1, the carrier of G))) mod p <> 0 by A1, A2, Lm5;
then reconsider E = the_subsets_of_card (k1, the carrier of G) as non empty finite set by NAT_D:26;
set LO9 = the_extension_of_left_operation_of (k1,(the_left_operation_of G));
reconsider T = the_extension_of_left_operation_of (k1,(the_left_operation_of G)) as LeftOperation of G,E ;
ex X being Element of E st (card (the_orbit_of (X,T))) mod p <> 0

proof

consider f being FinSequence such that
A4: rng f = the_orbits_of T and
A5: f is one-to-one by FINSEQ_4:58;
reconsider f = f as FinSequence of the_orbits_of T by A4, FINSEQ_1:def 4;
deffunc H₁( set ) -> set = card (f . $1);
consider pf being FinSequence such that
A6: ( len pf = len f & ( for i being Nat st i in dom pf holds
pf . i = H₁(i) ) ) from FINSEQ_1:sch 2();
for x being object st x in rng pf holds
x in NAT

proof

let x be object ; :: thesis: ( x in rng pf implies x in NAT )
assume x in rng pf ; :: thesis: x in NAT
then consider i being Nat such that
A7: i in dom pf and
A8: pf . i = x by FINSEQ_2:10;
i in dom f by A6, A7, FINSEQ_3:29;
then f . i in the_orbits_of T by A4, FUNCT_1:3;
then consider X being Subset of E such that
A9: f . i = X and
ex x9 being Element of E st X = the_orbit_of (x9,T) ;
x = card X by A6, A7, A8, A9;
hence x in NAT ; :: thesis: verum

end;

then rng pf c= NAT ;
then reconsider c = pf as FinSequence of NAT by FINSEQ_1:def 4;
deffunc H₂( set ) -> set = (c . $1) / p;
consider c9 being FinSequence such that
A10: ( len c9 = len c & ( for i being Nat st i in dom c9 holds
c9 . i = H₂(i) ) ) from FINSEQ_1:sch 2();
assume A11: for X being Element of E holds (card (the_orbit_of (X,T))) mod p = 0 ; :: thesis: contradiction
for x being object st x in rng c9 holds
x in NAT

proof

reconsider p99 = p9 as Real ;
let x be object ; :: thesis: ( x in rng c9 implies x in NAT )
assume x in rng c9 ; :: thesis: x in NAT
then consider i being Nat such that
A12: i in dom c9 and
A13: c9 . i = x by FINSEQ_2:10;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
i in dom f by A6, A10, A12, FINSEQ_3:29;
then f . i in the_orbits_of T by A4, FUNCT_1:3;
then consider X being Subset of E such that
A14: f . i = X and
A15: ex x9 being Element of E st X = the_orbit_of (x9,T) ;
dom pf = dom c9 by A10, FINSEQ_3:29;
then c . i = card X by A6, A12, A14;
then A16: (c . i) mod p = 0 by A11, A15;
set q = (c . i) div p9;
c . i = (p9 * ((c . i) div p9)) + ((c . i) mod p9) by NAT_D:2
.= p9 * ((c . i) div p9) by A16 ;
then consider q being Nat such that
A17: c . i = p * q ;
x = (p99 * q) / p99 by A10, A12, A13, A17
.= (p99 / p99) * q by XCMPLX_1:74
.= 1 * q by XCMPLX_1:60 ;
hence x in NAT by ORDINAL1:def 12; :: thesis: verum

end;

then rng c9 c= NAT ;
then reconsider c9 = c9 as FinSequence of NAT by FINSEQ_1:def 4;
A18: dom c = Seg (len c9) by A10, FINSEQ_1:def 3
.= dom c9 by FINSEQ_1:def 3
.= dom (p9 * c9) by VALUED_1:def 5 ;
for k being Nat st k in dom c holds
c . k = (p9 * c9) . k

proof

reconsider p99 = p9 as Real ;
let k be Nat; :: thesis: ( k in dom c implies c . k = (p9 * c9) . k )
assume A19: k in dom c ; :: thesis: c . k = (p9 * c9) . k
then k in dom c9 by A10, FINSEQ_3:29;
then p * (c9 . k) = p * ((c . k) / p9) by A10
.= (p99 * (c . k)) / p99 by XCMPLX_1:74
.= (p99 / p99) * (c . k) by XCMPLX_1:74
.= 1 * (c . k) by XCMPLX_1:60 ;
hence c . k = (p9 * c9) . k by A18, A19, VALUED_1:def 5; :: thesis: verum

end;

then A20: c = p9 * c9 by A18, FINSEQ_1:13;
for i being Element of NAT st i in dom pf holds
pf . i = H₁(i) by A6;
then card E = Sum c by A4, A5, A6, WEDDWITT:6;
then (card E) mod p = (p9 * (Sum c9)) mod p9 by A20, RVSUM_1:87
.= 0 by NAT_D:13 ;
hence contradiction by A1, A2, A3, Lm5; :: thesis: verum

end;

then consider X being Element of E such that
A21: (card (the_orbit_of (X,T))) mod p <> 0 ;
set HX = the_strict_stabilizer_of (X,T);
card (the_orbit_of (X,T)) = Index (the_strict_stabilizer_of (X,T)) by Th8;
then A22: (index (the_strict_stabilizer_of (X,T))) mod p <> 0 by A21, GROUP_2:def 18;

A23: now :: thesis: not p divides index (the_strict_stabilizer_of (X,T))

assume p divides index (the_strict_stabilizer_of (X,T)) ; :: thesis: contradiction
then ex t being Nat st index (the_strict_stabilizer_of (X,T)) = p * t by NAT_D:def 3;
hence contradiction by A22, NAT_D:13; :: thesis: verum

end;

take the_strict_stabilizer_of (X,T) ; :: thesis: the_strict_stabilizer_of (X,T) is_Sylow_p-subgroup_of_prime p
X in { X9 where X9 is Subset of the carrier of G : card X9 = k1 } ;
then A24: ex X9 being Subset of the carrier of G st
( X9 = X & card X9 = k1 ) ;
reconsider H = the_strict_stabilizer_of (X,T) as finite Group ;
A25: the carrier of (the_strict_stabilizer_of (X,T)) = { g where g is Element of G : (T ^ g) .: {X} = {X} } by Def10;
reconsider X = X as non empty Subset of G by A24;
set x = the Element of X;
reconsider x = the Element of X as Element of G ;
k1 divides card G by A1, NAT_D:def 3;
then k1 <= card G by NAT_D:7;
then card k1 <= card the carrier of G ;
then A26: Segm (card k1) c= Segm (card the carrier of G) by NAT_1:39;

now :: thesis: for z being object st z in the carrier of H holds
z in X * (x ")

reconsider X1 = X as Element of E ;
let z be object ; :: thesis: ( z in the carrier of H implies z in X * (x ") )
assume z in the carrier of H ; :: thesis: z in X * (x ")
then consider g being Element of G such that
A27: z = g and
A28: (T ^ g) .: {X} = {X} by A25;
dom (T ^ g) = E by FUNCT_2:def 1;
then Im ((T ^ g),X) = {((T ^ g) . X)} by FUNCT_1:59;
then A29: (T ^ g) . X = X by A28, ZFMISC_1:3;
set h = g * x;
T . g = the_extension_of_left_translation_of (k1,g,(the_left_operation_of G)) by A26, Def5;
then A30: (T ^ g) . X1 = ((the_left_operation_of G) ^ g) .: X1 by A26, Def4;
reconsider LO = the_left_operation_of G as LeftOperation of G, the carrier of G ;
A31: LO ^ g = the_left_translation_of g by Def2;
ex x9 being set st
( x9 in dom (LO ^ g) & x9 in X & g * x = (LO ^ g) . x9 )

proof

reconsider x9 = x as set ;
take x9 ; :: thesis: ( x9 in dom (LO ^ g) & x9 in X & g * x = (LO ^ g) . x9 )
dom (LO ^ g) = the carrier of G by FUNCT_2:def 1;
hence ( x9 in dom (LO ^ g) & x9 in X ) ; :: thesis: g * x = (LO ^ g) . x9
thus g * x = (LO ^ g) . x9 by A31, TOPGRP_1:def 1; :: thesis: verum

end;

then A32: g * x in (LO ^ g) .: X by FUNCT_1:def 6;
(g * x) * (x ") = g * (x * (x ")) by GROUP_1:def 3
.= g * (1_ G) by GROUP_1:def 5
.= z by A27, GROUP_1:def 4 ;
hence z in X * (x ") by A29, A30, A32, GROUP_2:28; :: thesis: verum

end;

then the carrier of H c= X * (x ") ;
then card the carrier of H <= card (X * (x ")) by NAT_1:43;
then A33: card H <= p |^ r by A24, Lm7;
(p |^ r) * m = (card (the_strict_stabilizer_of (X,T))) * (index (the_strict_stabilizer_of (X,T))) by A1, GROUP_2:147;
then p |^ r divides card H by A2, A23, Lm6;
then A34: p |^ r <= card H by NAT_D:7;
then card H = p |^ r by A33, XXREAL_0:1;
then A35: H is p -group ;
index (the_strict_stabilizer_of (X,T)) = ((index (the_strict_stabilizer_of (X,T))) * (card (the_strict_stabilizer_of (X,T)))) * (1 / (card (the_strict_stabilizer_of (X,T)))) by XCMPLX_1:107
.= ((p |^ r) * m) * (1 / (card (the_strict_stabilizer_of (X,T)))) by A1, GROUP_2:147
.= ((p9 |^ r) * m) * (1 / (p9 |^ r)) by A34, A33, XXREAL_0:1
.= m * ((p9 |^ r) * (1 / (p9 |^ r)))
.= m * ((p9 |^ r) / (p9 |^ r)) by XCMPLX_1:99
.= m by XCMPLX_1:88 ;
hence the_strict_stabilizer_of (X,T) is_Sylow_p-subgroup_of_prime p by A2, A35; :: thesis: verum