let IT1, IT2 be Function of (the_sylow_p-subgroups_of_prime (p,G)),(the_sylow_p-subgroups_of_prime (p,G)); :: 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 = IT1 . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) ) & ( 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 = IT2 . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) ) implies IT1 = IT2 )
assume A23: ( ( 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 = IT1 . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) ) & ( 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 = IT2 . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) ) ) ; :: thesis: IT1 = IT2
let x be Element of the_sylow_p-subgroups_of_prime (p,G); :: according to FUNCT_2:def 8 :: thesis: ^ = ^
( ex P12 being Element of the_sylow_p-subgroups_of_prime (p,G) ex H11, H12 being strict Subgroup of G ex g1 being Element of G st
( P12 = IT1 . x & x = H11 & P12 = H12 & h " = g1 & H12 = H11 |^ g1 ) & ex P22 being Element of the_sylow_p-subgroups_of_prime (p,G) ex H21, H22 being strict Subgroup of G ex g2 being Element of G st
( P22 = IT2 . x & x = H21 & P22 = H22 & h " = g2 & H22 = H21 |^ g2 ) ) by A23;
hence IT1 . x = IT2 . x ; :: thesis: verum