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 ) } ;

let x, y1, y2 be object ; :: thesis:
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:
then consider P19, P29 being Element of Left_Cosets P such that
A2: [x,y1] = [P19,P29] and
A3: ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P19 & A2 = P29 & g = h ) ;
A4: x = P19 by A2, XTUPLE_0:1;
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:
then consider P199, P299 being Element of Left_Cosets P such that
A5: [x,y2] = [P199,P299] and
A6: ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P199 & A2 = P299 & g = h ) ;
x = P199 by A5, XTUPLE_0:1;
hence y1 = y2 by A2, A3, A5, A6, A4, XTUPLE_0:1; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:
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:
then consider P1, P2 being Element of Left_Cosets P such that
A7: x = [P1,P2] and
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 object ;
take y = y; :: thesis:
take z = z; :: thesis:
thus x = [y,z] by A7; :: thesis:

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 :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

reconsider g = h as Element of G by GROUP_2:42;
assume x in Left_Cosets P ; :: thesis:
then consider a being Element of G such that
A8: x = a * P by GROUP_2:def 15;
reconsider P1 = x as Element of Left_Cosets P by A8, GROUP_2:def 15;
reconsider y = g * (a * P) as object ;
take y = y; :: thesis:
g * (a * P) = (g * a) * P by GROUP_2:105;
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 A8;
hence [x,y] in f ; :: thesis:

end;

given y being object such that A9: [x,y] in f ; :: thesis:
consider P1, P2 being Element of Left_Cosets P such that
A10: [x,y] = [P1,P2] and
ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) by A9;
x = P1 by A10, XTUPLE_0:1;
hence x in Left_Cosets P ; :: thesis:

end;

then A12: dom f = Left_Cosets P by XTUPLE_0:def 12;

now :: thesis:

let y be object ; :: thesis:
assume y in rng f ; :: thesis:
then consider x being object such that
A14: ( x in dom f & y = f . x ) by FUNCT_1:def 3;
[x,y] in f by A14, FUNCT_1:1;
then consider P1, P2 being Element of Left_Cosets P such that
A15: [x,y] = [P1,P2] and
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 by A15, XTUPLE_0:1;
hence y in Left_Cosets P ; :: thesis:

end;

then rng f c= Left_Cosets P ;
then reconsider f = f as Function of (Left_Cosets P),(Left_Cosets P) by A12, FUNCT_2:2;
take f ; :: thesis:
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:

proof

let P1 be Element of Left_Cosets P; :: thesis:
set P2 = f . P1;
[P1,(f . P1)] in f by A12, FUNCT_1:1;
then consider P19, P29 being Element of Left_Cosets P such that
A16: [P1,(f . P1)] = [P19,P29] and
A17: ex A1, A2 being Subset of G ex g being Element of G st
( A2 = g * A1 & A1 = P19 & A2 = P29 & h = g ) ;
reconsider P2 = f . P1 as Element of Left_Cosets P ;
consider A1, A2 being Subset of G, g being Element of G such that
A18: ( A2 = g * A1 & A1 = P19 ) and
A2 = P29 and
A19: h = g by A17;
take P2 ; :: thesis:
take A1 ; :: thesis:
take A2 ; :: thesis:
take g ; :: thesis:
thus P2 = f . P1 ; :: thesis:
thus ( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) by A16, A17, A18, A19, XTUPLE_0:1; :: thesis:

end;