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

proof

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

end;

consider f being Function such that
A3: dom f = a * H and
A4: for x being set st x in a * H holds
S₁[x,f . x] from CLASSES1:sch 1(A2);
A5: rng f = H * b

proof

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in H * b )
assume x in rng f ; :: thesis: x in H * b
then consider y being set such that
A6: y in dom f and
A7: f . y = x by FUNCT_1:def 5;
consider g being Element of G such that
A8: y = g and
A9: x = ((a " ) * g) * b by A3, A4, A6, A7;
consider g1 being Element of G such that
A10: g = a * g1 and
A11: g1 in H by A3, A6, A8, Th125;
x = (((a " ) * a) * g1) * b by A9, A10, GROUP_1:def 4
.= ((1_ G) * g1) * b by GROUP_1:def 6
.= g1 * b by GROUP_1:def 5 ;
hence x in H * b by A11, Th126; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in H * b or x in rng f )
assume x in H * b ; :: thesis: x in rng f
then consider g being Element of G such that
A12: x = g * b and
A13: g in H by Th126;
A14: a * g in dom f by A3, A13, Th125;
then ex g1 being Element of G st
( g1 = a * g & f . (a * g) = ((a " ) * g1) * b ) by A3, A4;
then f . (a * g) = (((a " ) * a) * g) * b by GROUP_1:def 4
.= ((1_ G) * g) * b by GROUP_1:def 6
.= x by A12, GROUP_1:def 5 ;
hence x in rng f by A14, FUNCT_1:def 5; :: 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
A15: x in dom f and
A16: y in dom f and
A17: f . x = f . y ; :: thesis: x = y
consider g1 being Element of G such that
A18: x = g1 and
A19: f . x = ((a " ) * g1) * b by A3, A4, A15;
consider g2 being Element of G such that
A20: y = g2 and
A21: f . y = ((a " ) * g2) * b by A3, A4, A16;
(a " ) * g1 = (a " ) * g2 by A17, A19, A21, GROUP_1:14;
hence x = y by A18, A20, GROUP_1:14; :: thesis: verum

end;

hence a * H,H * b are_equipotent by A3, A5, WELLORD2:def 4; :: thesis: verum