let IT1, IT2 be Function of (Left_Cosets P),(Left_Cosets P); :: thesis: ( ( for P1 being Element of Left_Cosets P ex P2 being Element of Left_Cosets P ex A1, A2 being Subset of G ex g being Element of G st
( P2 = IT1 . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) ) & ( for P1 being Element of Left_Cosets P ex P2 being Element of Left_Cosets P ex A1, A2 being Subset of G ex g being Element of G st
( P2 = IT2 . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) ) implies IT1 = IT2 )
assume A20: ( ( for P1 being Element of Left_Cosets P ex P2 being Element of Left_Cosets P ex A1, A2 being Subset of G ex g being Element of G st
( P2 = IT1 . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) ) & ( for P1 being Element of Left_Cosets P ex P2 being Element of Left_Cosets P ex A1, A2 being Subset of G ex g being Element of G st
( P2 = IT2 . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) ) ) ; :: thesis: IT1 = IT2
let x be Element of Left_Cosets P; :: according to FUNCT_2:def 8 :: thesis: ^ = ^
( ex P12 being Element of Left_Cosets P ex A11, A12 being Subset of G ex g1 being Element of G st
( P12 = IT1 . x & A12 = g1 * A11 & A11 = x & A12 = P12 & g1 = h ) & ex P22 being Element of Left_Cosets P ex A21, A22 being Subset of G ex g2 being Element of G st
( P22 = IT2 . x & A22 = g2 * A21 & A21 = x & A22 = P22 & g2 = h ) ) by A20;
hence ^ = ^ ; :: thesis: verum