set f = { [P1,P2] where P1, P2 is Element of Left_Cosets P : ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) } ;

A1: now

let x, y1, y2 be set ; :: thesis: ( [x,y1] in { [P1,P2] where P1, P2 is Element of Left_Cosets P : ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) } & [x,y2] in { [P1,P2] where P1, P2 is Element of Left_Cosets P : ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) } implies y1 = y2 )
assume [x,y1] in { [P1,P2] where P1, P2 is Element of Left_Cosets P : ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) } ; :: thesis: ( [x,y2] in { [P1,P2] where P1, P2 is Element of Left_Cosets P : ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) } implies y1 = y2 )
then consider P1', P2' being Element of Left_Cosets P such that
A2: ( [x,y1] = [P1',P2'] & ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P1' & A2 = P2' & g = h ) ) ;
assume [x,y2] in { [P1,P2] where P1, P2 is Element of Left_Cosets P : ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) } ; :: thesis: y1 = y2
then consider P1'', P2'' being Element of Left_Cosets P such that
A3: ( [x,y2] = [P1'',P2''] & ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P1'' & A2 = P2'' & g = h ) ) ;
A4: ( x = P1'' & y2 = P2'' ) by A3, ZFMISC_1:33;
( x = P1' & y1 = P2' ) by A2, ZFMISC_1:33;
hence y1 = y2 by A2, A3, A4; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in { [P1,P2] where P1, P2 is Element of Left_Cosets P : ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) } implies ex y, z being set st x = [y,z] )
assume x in { [P1,P2] where P1, P2 is Element of Left_Cosets P : ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) } ; :: thesis: ex y, z being set st x = [y,z]
then consider P1, P2 being Element of Left_Cosets P such that
A5: ( x = [P1,P2] & ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) ) ;
reconsider y = P1, z = P2 as set ;
take y = y; :: thesis: ex z being set st x = [y,z]
take z = z; :: thesis: x = [y,z]
thus x = [y,z] by A5; :: thesis: verum

end;

then reconsider f = { [P1,P2] where P1, P2 is Element of Left_Cosets P : ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) } as Function by A1, FUNCT_1:def 1, RELAT_1:def 1;

now

let x be set ; :: thesis: ( ( x in Left_Cosets P implies ex y being set st [x,y] in f ) & ( ex y being set st [x,y] in f implies x in Left_Cosets P ) )

hereby :: thesis: ( ex y being set st [x,y] in f implies x in Left_Cosets P )

assume x in Left_Cosets P ; :: thesis: ex y being set st [x,y] in f
then consider a being Element of G such that
A6: x = a * P by GROUP_2:def 15;
reconsider g = h as Element of G by GROUP_2:51;
reconsider y = g * (a * P) as set ;
take y = y; :: thesis: [x,y] in f
reconsider P1 = x as Element of Left_Cosets P by A6, GROUP_2:def 15;
g * (a * P) = (g * a) * P by GROUP_2:127;
then reconsider P2 = y as Element of Left_Cosets P by GROUP_2:def 15;
ex A1, A2 being Subset of G st
( A2 = g * A1 & A1 = P1 & A2 = P2 ) by A6;
hence [x,y] in f ; :: thesis: verum

end;

given y being set such that A7: [x,y] in f ; :: thesis: x in Left_Cosets P
consider P1, P2 being Element of Left_Cosets P such that
A8: ( [x,y] = [P1,P2] & ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) ) by A7;
( x = P1 & not Left_Cosets P is empty ) by A8, GROUP_2:165, ZFMISC_1:33;
hence x in Left_Cosets P ; :: thesis: verum

end;

then A9: dom f = Left_Cosets P by RELAT_1:def 4;

now

let y be set ; :: thesis: ( y in rng f implies y in Left_Cosets P )
assume y in rng f ; :: thesis: y in Left_Cosets P
then consider x being set such that
A10: ( x in dom f & y = f . x ) by FUNCT_1:def 5;
[x,y] in f by A10, FUNCT_1:8;
then consider P1, P2 being Element of Left_Cosets P such that
A11: ( [x,y] = [P1,P2] & ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P1 & A2 = P2 & h = g ) ) ;
( y = P2 & not Left_Cosets P is empty ) by A11, GROUP_2:165, ZFMISC_1:33;
hence y in Left_Cosets P ; :: thesis: verum

end;

then rng f c= Left_Cosets P by TARSKI:def 3;
then reconsider f = f as Function of (Left_Cosets P),(Left_Cosets P) by A9, FUNCT_2:4;
take f ; :: 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 = f . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h )
thus 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 = f . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) :: thesis: verum

proof

let P1 be Element of Left_Cosets P; :: thesis: ex P2 being Element of Left_Cosets P ex A1, A2 being Subset of G ex g being Element of G st
( P2 = f . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h )
set P2 = f . P1;
not Left_Cosets P is empty by GROUP_2:165;
then [P1,(f . P1)] in f by A9, FUNCT_1:8;
then consider P1', P2' being Element of Left_Cosets P such that
A12: ( [P1,(f . P1)] = [P1',P2'] & ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P1' & A2 = P2' & h = g ) ) ;
consider A1, A2 being Subset of G, g being Element of G such that
A13: ( A2 = g * A1 & A1 = P1' & A2 = P2' & h = g ) by A12;
reconsider P2 = f . P1 as Element of Left_Cosets P by A12, ZFMISC_1:33;
take P2 ; :: thesis: ex A1, A2 being Subset of G ex g being Element of G st
( P2 = f . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h )
take A1 ; :: thesis: ex A2 being Subset of G ex g being Element of G st
( P2 = f . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h )
take A2 ; :: thesis: ex g being Element of G st
( P2 = f . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h )
take g ; :: thesis: ( P2 = f . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h )
thus P2 = f . P1 ; :: thesis: ( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h )
thus ( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) by A12, A13, ZFMISC_1:33; :: thesis: verum

end;