let G be Group; :: thesis: for H being Subgroup of G holds Left_Cosets H, Right_Cosets H are_equipotent
let H be Subgroup of G; :: thesis: Left_Cosets H, Right_Cosets H are_equipotent
defpred S₁[ set , set ] means ex g being Element of G st
( $1 = g * H & $2 = H * (g " ) );
A6: for x being set st x in Left_Cosets H holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in Left_Cosets H implies ex y being set st S₁[x,y] )
assume x in Left_Cosets H ; :: thesis: ex y being set st S₁[x,y]
then consider g being Element of G such that
A7: x = g * H by Def15;
reconsider y = H * (g " ) as set ;
take y ; :: thesis: S₁[x,y]
take g ; :: thesis: ( x = g * H & y = H * (g " ) )
thus ( x = g * H & y = H * (g " ) ) by A7; :: thesis: verum

end;

consider f being Function such that
A8: dom f = Left_Cosets H and
A9: for x being set st x in Left_Cosets H holds
S₁[x,f . x] from CLASSES1:sch 1(A6);
A10: rng f = Right_Cosets H

proof

thus rng f c= Right_Cosets H :: according to XBOOLE_0:def 10 :: thesis: Right_Cosets H c= rng f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in Right_Cosets H )
assume x in rng f ; :: thesis: x in Right_Cosets H
then consider y being set such that
A11: y in dom f and
A12: f . y = x by FUNCT_1:def 5;
ex g being Element of G st
( y = g * H & f . y = H * (g " ) ) by A8, A9, A11;
hence x in Right_Cosets H by A12, Def16; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Right_Cosets H or x in rng f )
assume A13: x in Right_Cosets H ; :: thesis: x in rng f
then reconsider A = x as Subset of G ;
consider g being Element of G such that
A14: A = H * g by A13, Def16;
A15: (g " ) * H in Left_Cosets H by Def15;
then A16: f . ((g " ) * H) in rng f by A8, FUNCT_1:def 5;
consider a being Element of G such that
A17: (g " ) * H = a * H and
A18: f . ((g " ) * H) = H * (a " ) by A9, A15;
(a " ) * (g " ) in H by A17, Th137;
hence x in rng f by A14, A16, A18, Th143; :: thesis: verum

end;

f is one-to-one

proof

let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in dom f or not b₁ in dom f or not f . x = f . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A19: x in dom f and
A20: y in dom f and
A21: f . x = f . y ; :: thesis: x = y
consider a being Element of G such that
A22: x = a * H and
A23: f . x = H * (a " ) by A8, A9, A19;
consider b being Element of G such that
A24: y = b * H and
A25: f . y = H * (b " ) by A8, A9, A20;
(b " ) * ((a " ) " ) in H by A21, A23, A25, Th143;
then (b " ) * a in H by GROUP_1:19;
hence x = y by A22, A24, Th137; :: thesis: verum

end;

hence Left_Cosets H, Right_Cosets H are_equipotent by A8, A10, WELLORD2:def 4; :: thesis: verum