let G be finite Group; :: thesis:
let p be natural prime number ; :: thesis:
reconsider p9 = p as prime Element of NAT by ORDINAL1:def 12;
A1: for H, P being Subgroup of G st H is p -group & P is_Sylow_p-subgroup_of_prime p holds
ex g being Element of G st carr H c= carr (P |^ g)

let H, P be Subgroup of G; :: thesis:
set H9 = H;
set E = Left_Cosets P;
set T = the_left_operation_of (H,P);
reconsider E = Left_Cosets P as non empty finite set by GROUP_2:135;
reconsider T = the_left_operation_of (H,P) as LeftOperation of H,E ;
assume H is p -group ; :: thesis:
then A2: (card (the_fixed_points_of T)) mod p = (card E) mod p by Th11;
assume P is_Sylow_p-subgroup_of_prime p ; :: thesis:
then A3: not p divides index P by Def19;

assume (card E) mod p = 0 ; :: thesis:
then ( ex t being Nat st
( card E = (p * t) + 0 & 0 < p ) or ( 0 = 0 & p = 0 ) ) by NAT_D:def 2;
then p9 divides card E by NAT_D:def 3;
hence contradiction by A3, GROUP_2:def 18; :: thesis:

end;

then card (the_fixed_points_of T) <> 0 by A2, NAT_D:26;
then consider x being set such that
A4: x in the_fixed_points_of T by CARD_1:27, XBOOLE_0:def 1;
x in { x9 where x9 is Element of E : x9 is_fixed_under T } by A4, Def13;
then consider x9 being Element of E such that
x = x9 and
A5: x9 is_fixed_under T ;
x9 in Left_Cosets P ;
then consider g9 being Element of G such that
A6: x9 = g9 * P by GROUP_2:def 15;
set g = g9 " ;
take g9 " ; :: thesis:

reconsider P1 = x9 as Element of Left_Cosets P ;
let y be set ; :: thesis:
assume y in carr H ; :: thesis:
then reconsider h = y as Element of H ;
reconsider h9 = h as Element of H ;
consider P2 being Element of Left_Cosets P, A1, A2 being Subset of G, g99 being Element of G such that
A7: ( P2 = (the_left_translation_of (h9,P)) . P1 & A2 = g99 * A1 & A1 = P1 & A2 = P2 ) and
A8: g99 = h9 by Def8;
(the_left_operation_of (H,P)) . h9 = the_left_translation_of (h9,P) by Def9;
then A9: (g9 * P) * (g9 ") = (g99 * (g9 * P)) * (g9 ") by A5, A6, A7, Def12
.= g99 * ((g9 * P) * (g9 ")) by GROUP_2:33 ;
g99 in (g9 * P) * (g9 ")

1_ G in P by GROUP_2:46;
then A10: 1_ G in carr P by STRUCT_0:def 5;
g9 = g9 * (1_ G) by GROUP_1:def 4;
then ( g9 * (g9 ") = 1_ G & g9 in g9 * P ) by A10, GROUP_1:def 5, GROUP_2:27;
then A11: ( g99 = g99 * (1_ G) & 1_ G in (g9 * P) * (g9 ") ) by GROUP_1:def 4, GROUP_2:28;
assume not g99 in (g9 * P) * (g9 ") ; :: thesis:
hence contradiction by A9, A11, GROUP_2:27; :: thesis:

end;

hence y in (g9 * P) * (g9 ") by A8; :: thesis:

end;

then carr H c= (((g9 ") ") * P) * (g9 ") by TARSKI:def 3;
hence carr H c= carr (P |^ (g9 ")) by GROUP_3:59; :: thesis:

end;

thus for H being Subgroup of G st H is p -group holds
ex P being Subgroup of G st
( P is_Sylow_p-subgroup_of_prime p & H is Subgroup of P ) :: thesis:

let H be Subgroup of G; :: thesis:
consider P9 being strict Subgroup of G such that
A12: P9 is_Sylow_p-subgroup_of_prime p by Th12;
assume H is p -group ; :: thesis:
then consider g being Element of G such that
A13: carr H c= carr (P9 |^ g) by A1, A12;
set P = P9 |^ g;
take P9 |^ g ; :: thesis:
set H2 = P9 |^ g;
reconsider H2 = P9 |^ g as finite Group ;
A14: card P9 = card (P9 |^ g) by GROUP_3:66;
P9 is p -group by A12, Def19;
then consider H1 being finite Group such that
A15: P9 = H1 and
A16: H1 is p -group ;
ex r being natural number st card H1 = p |^ r by A16, Def17;
then A17: H2 is p -group by A15, A14, Def17;
A18: not p divides index P9 by A12, Def19;
(card (P9 |^ g)) * (index (P9 |^ g)) = card G by GROUP_2:147
.= (card (P9 |^ g)) * (index P9) by A14, GROUP_2:147 ;
then not p divides index (P9 |^ g) by A18, XCMPLX_1:5;
hence P9 |^ g is_Sylow_p-subgroup_of_prime p by A17, Def19; :: thesis:
thus H is Subgroup of P9 |^ g by A13, GROUP_2:57; :: thesis:

end;

let P1, P2 be Subgroup of G; :: thesis:
assume A19: P1 is_Sylow_p-subgroup_of_prime p ; :: thesis:
then A20: P1 is p -group by Def19;
then consider H1 being finite Group such that
A21: P1 = H1 and
A22: H1 is p -group ;
A23: not p divides index P1 by A19, Def19;
consider r1 being natural number such that
A24: card H1 = p |^ r1 by A22, Def17;
assume A25: P2 is_Sylow_p-subgroup_of_prime p ; :: thesis:
then A26: not p divides index P2 by Def19;
P2 is p -group by A25, Def19;
then consider H2 being finite Group such that
A27: P2 = H2 and
A28: H2 is p -group ;
consider r2 being natural number such that
A29: card H2 = p |^ r2 by A28, Def17;
A30: card G = (card P2) * (index P2) by GROUP_2:147;
then A31: (p |^ r1) * (index P1) = (p |^ r2) * (index P2) by A21, A24, A27, A29, GROUP_2:147;

assume A32: r1 <> r2 ; :: thesis:

per cases by A32, XXREAL_0:1;

suppose A33: r1 > r2 ; :: thesis:

set r = r1 -' r2;
A34: r1 - r2 > r2 - r2 by A33, XREAL_1:9;
then A35: r1 -' r2 = r1 - r2 by XREAL_0:def 2;
then consider k being Nat such that
A36: r1 -' r2 = k + 1 by A34, NAT_1:6;
r1 = r2 + (r1 -' r2) by A35;
then p9 |^ r1 = (p9 |^ r2) * (p9 |^ (r1 -' r2)) by NEWTON:8;
then (p9 |^ r2) * ((p9 |^ (r1 -' r2)) * (index P1)) = (p9 |^ r2) * (index P2) by A31;
then (p9 |^ (r1 -' r2)) * (index P1) = index P2 by XCMPLX_1:5;
then ((p |^ k) * p) * (index P1) = index P2 by A36, NEWTON:6;
then p * ((p |^ k) * (index P1)) = index P2 ;
hence contradiction by A26, NAT_D:def 3; :: thesis:

end;

suppose A37: r1 < r2 ; :: thesis:

set r = r2 -' r1;
A38: r2 - r1 > r1 - r1 by A37, XREAL_1:9;
then A39: r2 -' r1 = r2 - r1 by XREAL_0:def 2;
then consider k being Nat such that
A40: r2 -' r1 = k + 1 by A38, NAT_1:6;
r2 = r1 + (r2 -' r1) by A39;
then p9 |^ r2 = (p9 |^ r1) * (p9 |^ (r2 -' r1)) by NEWTON:8;
then (p9 |^ r1) * ((p9 |^ (r2 -' r1)) * (index P2)) = (p9 |^ r1) * (index P1) by A21, A24, A27, A29, A30, GROUP_2:147;
then (p9 |^ (r2 -' r1)) * (index P2) = index P1 by XCMPLX_1:5;
then ((p |^ k) * p) * (index P2) = index P1 by A40, NEWTON:6;
then p * ((p |^ k) * (index P2)) = index P1 ;
hence contradiction by A23, NAT_D:def 3; :: thesis:

end;

end;

end;

then A41: card (carr P1) = card (carr P2) by A21, A24, A27, A29;
consider g being Element of G such that
A42: carr P1 c= carr (P2 |^ g) by A1, A20, A25;
card (carr P2) = card P2
.= card (P2 |^ g) by GROUP_3:66
.= card (carr (P2 |^ g)) ;
then multMagma(# the carrier of P1, the multF of P1 #) = multMagma(# the carrier of (P2 |^ g), the multF of (P2 |^ g) #) by A42, A41, CARD_FIN:1, GROUP_2:59;
hence P1,P2 are_conjugated by GROUP_3:def 11; :: thesis: