set E = the_sylow_p-subgroups_of_prime (p,G);
set f = { [P1,P2] where P1, P2 is Element of the_sylow_p-subgroups_of_prime (p,G) : ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) } ;

A1: now :: thesis: for x, y1, y2 being object st [x,y1] in { [P1,P2] where P1, P2 is Element of the_sylow_p-subgroups_of_prime (p,G) : ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) } & [x,y2] in { [P1,P2] where P1, P2 is Element of the_sylow_p-subgroups_of_prime (p,G) : ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) } holds
y1 = y2

let x, y1, y2 be object ; :: thesis: ( [x,y1] in { [P1,P2] where P1, P2 is Element of the_sylow_p-subgroups_of_prime (p,G) : ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) } & [x,y2] in { [P1,P2] where P1, P2 is Element of the_sylow_p-subgroups_of_prime (p,G) : ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) } implies y1 = y2 )
assume [x,y1] in { [P1,P2] where P1, P2 is Element of the_sylow_p-subgroups_of_prime (p,G) : ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) } ; :: thesis: ( [x,y2] in { [P1,P2] where P1, P2 is Element of the_sylow_p-subgroups_of_prime (p,G) : ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) } implies y1 = y2 )
then consider P19, P29 being Element of the_sylow_p-subgroups_of_prime (p,G) such that
A2: [x,y1] = [P19,P29] and
A3: ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P19 = H1 & P29 = H2 & h " = g & H2 = H1 |^ g ) ;
A4: x = P19 by A2, XTUPLE_0:1;
assume [x,y2] in { [P1,P2] where P1, P2 is Element of the_sylow_p-subgroups_of_prime (p,G) : ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) } ; :: thesis: y1 = y2
then consider P199, P299 being Element of the_sylow_p-subgroups_of_prime (p,G) such that
A5: [x,y2] = [P199,P299] and
A6: ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P199 = H1 & P299 = H2 & h " = g & H2 = H1 |^ g ) ;
x = P199 by A5, XTUPLE_0:1;
hence y1 = y2 by A2, A3, A5, A6, A4, XTUPLE_0:1; :: thesis: verum

end;

now :: thesis: for x being object st x in { [P1,P2] where P1, P2 is Element of the_sylow_p-subgroups_of_prime (p,G) : ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) } holds
ex y, z being object st x = [y,z]

let x be object ; :: thesis: ( x in { [P1,P2] where P1, P2 is Element of the_sylow_p-subgroups_of_prime (p,G) : ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) } implies ex y, z being object st x = [y,z] )
assume x in { [P1,P2] where P1, P2 is Element of the_sylow_p-subgroups_of_prime (p,G) : ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) } ; :: thesis: ex y, z being object st x = [y,z]
then consider P1, P2 being Element of the_sylow_p-subgroups_of_prime (p,G) such that
A7: x = [P1,P2] and
ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) ;
reconsider y = P1, z = P2 as object ;
take y = y; :: thesis: ex z being object st x = [y,z]
take z = z; :: thesis: x = [y,z]
thus x = [y,z] by A7; :: thesis: verum

end;

then reconsider f = { [P1,P2] where P1, P2 is Element of the_sylow_p-subgroups_of_prime (p,G) : ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) } as Function by A1, FUNCT_1:def 1, RELAT_1:def 1;

now :: thesis: for y being object st y in rng f holds
y in the_sylow_p-subgroups_of_prime (p,G)

let y be object ; :: thesis: ( y in rng f implies y in the_sylow_p-subgroups_of_prime (p,G) )
assume y in rng f ; :: thesis: y in the_sylow_p-subgroups_of_prime (p,G)
then consider x being object such that
A8: [x,y] in f by XTUPLE_0:def 13;
consider P1, P2 being Element of the_sylow_p-subgroups_of_prime (p,G) such that
A9: [x,y] = [P1,P2] and
ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) by A8;
y = P2 by A9, XTUPLE_0:1;
hence y in the_sylow_p-subgroups_of_prime (p,G) ; :: thesis: verum

end;

then A10: rng f c= the_sylow_p-subgroups_of_prime (p,G) ;

now :: thesis: for x being object holds
( ( x in the_sylow_p-subgroups_of_prime (p,G) implies ex y being object st [x,y] in f ) & ( ex y being object st [x,y] in f implies x in the_sylow_p-subgroups_of_prime (p,G) ) )

let x be object ; :: thesis: ( ( x in the_sylow_p-subgroups_of_prime (p,G) implies ex y being object st [x,y] in f ) & ( ex y being object st [x,y] in f implies x in the_sylow_p-subgroups_of_prime (p,G) ) )

hereby :: thesis: ( ex y being object st [x,y] in f implies x in the_sylow_p-subgroups_of_prime (p,G) )

reconsider g = h " as Element of G by GROUP_2:42;
assume x in the_sylow_p-subgroups_of_prime (p,G) ; :: thesis: ex y being object st [x,y] in f
then reconsider P1 = x as Element of the_sylow_p-subgroups_of_prime (p,G) ;
P1 in the_sylow_p-subgroups_of_prime (p,G) ;
then consider H1 being Element of Subgroups G such that
A11: P1 = H1 and
A12: ex P being strict Subgroup of G st
( P = H1 & P is_Sylow_p-subgroup_of_prime p ) ;
reconsider H1 = H1 as strict Subgroup of G by A12;
H1 is p -group by A12;
then consider H9 being finite Group such that
A13: ( H1 = H9 & H9 is p -group ) ;
set H2 = H1 |^ g;
reconsider H2 = H1 |^ g as strict Subgroup of G ;
reconsider H99 = H2 as finite Group ;
( ex r being Nat st card H9 = p |^ r & card H9 = card H99 ) by A13, GROUP_3:66;
then A14: H99 is p -group ;
reconsider H29 = H2 as Element of Subgroups G by GROUP_3:def 1;
A15: card H1 = card H2 by GROUP_3:66;
A16: (card H1) * (index H1) = card G by GROUP_2:147
.= (card H1) * (index H2) by A15, GROUP_2:147 ;
not p divides index H1 by A12;
then not p divides index H2 by A16, XCMPLX_1:5;
then H2 is_Sylow_p-subgroup_of_prime p by A14;
then H29 in the_sylow_p-subgroups_of_prime (p,G) ;
then reconsider P2 = H2 as Element of the_sylow_p-subgroups_of_prime (p,G) ;
reconsider y = P2 as object ;
take y = y; :: thesis: [x,y] in f
thus [x,y] in f by A11; :: thesis: verum

end;

given y being object such that A17: [x,y] in f ; :: thesis: x in the_sylow_p-subgroups_of_prime (p,G)
consider P1, P2 being Element of the_sylow_p-subgroups_of_prime (p,G) such that
A18: [x,y] = [P1,P2] and
ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) by A17;
x = P1 by A18, XTUPLE_0:1;
hence x in the_sylow_p-subgroups_of_prime (p,G) ; :: thesis: verum

end;

then A19: dom f = the_sylow_p-subgroups_of_prime (p,G) by XTUPLE_0:def 12;
then reconsider f = f as Function of (the_sylow_p-subgroups_of_prime (p,G)),(the_sylow_p-subgroups_of_prime (p,G)) by A10, FUNCT_2:2;
take f ; :: thesis: for P1 being Element of the_sylow_p-subgroups_of_prime (p,G) ex P2 being Element of the_sylow_p-subgroups_of_prime (p,G) ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P2 = f . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g )
thus for P1 being Element of the_sylow_p-subgroups_of_prime (p,G) ex P2 being Element of the_sylow_p-subgroups_of_prime (p,G) ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P2 = f . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) :: thesis: verum

proof

let P1 be Element of the_sylow_p-subgroups_of_prime (p,G); :: thesis: ex P2 being Element of the_sylow_p-subgroups_of_prime (p,G) ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P2 = f . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g )
set P2 = f . P1;
[P1,(f . P1)] in f by A19, FUNCT_1:1;
then consider P19, P29 being Element of the_sylow_p-subgroups_of_prime (p,G) such that
A20: [P1,(f . P1)] = [P19,P29] and
A21: ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P19 = H1 & P29 = H2 & h " = g & H2 = H1 |^ g ) ;
reconsider P2 = f . P1 as Element of the_sylow_p-subgroups_of_prime (p,G) ;
consider H1, H2 being strict Subgroup of G, g being Element of G such that
A22: ( P19 = H1 & P29 = H2 & h " = g ) and
H2 = H1 |^ g by A21;
take P2 ; :: thesis: ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P2 = f . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g )
take H1 ; :: thesis: ex H2 being strict Subgroup of G ex g being Element of G st
( P2 = f . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g )
take H2 ; :: thesis: ex g being Element of G st
( P2 = f . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g )
take g ; :: thesis: ( P2 = f . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g )
thus P2 = f . P1 ; :: thesis: ( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g )
thus ( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) by A20, A21, A22, XTUPLE_0:1; :: thesis: verum

end;