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 that
A21: 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 ) and
A22: 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 9 :: thesis: ^ = ^
consider P12 being Element of the_sylow_p-subgroups_of_prime p,G, H11, H12 being strict Subgroup of G, g1 being Element of G such that
A23: ( P12 = IT1 . x & x = H11 & P12 = H12 & h " = g1 & H12 = H11 |^ g1 ) by A21;
consider P22 being Element of the_sylow_p-subgroups_of_prime p,G, H21, H22 being strict Subgroup of G, g2 being Element of G such that
A24: ( P22 = IT2 . x & x = H21 & P22 = H22 & h " = g2 & H22 = H21 |^ g2 ) by A22;
thus IT1 . x = IT2 . x by A23, A24; :: thesis: verum