let G be addGroup; :: 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₁[ object , object ] means ex g1 being Element of G st
( $1 = g1 & $2 = ((- a) + g1) + b );
A1: for x being object st x in a + H holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in a + H implies ex y being object st S₁[x,y] )
assume x in a + H ; :: thesis: ex y being object 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
A2: dom f = a + H and
A3: for x being object st x in a + H holds
S₁[x,f . x] from CLASSES1:sch 1(A1);
A4: 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 object ; :: 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 object such that
A5: y in dom f and
A6: f . y = x by FUNCT_1:def 3;
consider g being Element of G such that
A7: y = g and
A8: x = ((- a) + g) + b by A2, A3, A5, A6;
consider g1 being Element of G such that
A9: g = a + g1 and
A10: g1 in H by A2, A5, A7, Th103;
x = (((- a) + a) + g1) + b by A8, A9, RLVECT_1:def 3
.= ((0_ G) + g1) + b by Def5
.= g1 + b by Def4 ;
hence x in H + b by A10, Th104; :: thesis: verum

end;

let x be object ; :: 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
A11: x = g + b and
A12: g in H by Th104;
A13: a + g in dom f by A2, A12, Th103;
ex g1 being Element of G st
( g1 = a + g & f . (a + g) = ((- a) + g1) + b ) by A3, A12, Th103;
then f . (a + g) = (((- a) + a) + g) + b by RLVECT_1:def 3
.= ((0_ G) + g) + b by Def5
.= x by A11, Def4 ;
hence x in rng f by A13, FUNCT_1:def 3; :: thesis: verum

end;

f is one-to-one

proof

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A14: x in dom f and
A15: y in dom f and
A16: f . x = f . y ; :: thesis: x = y
consider g2 being Element of G such that
A17: y = g2 and
A18: f . y = ((- a) + g2) + b by A2, A3, A15;
consider g1 being Element of G such that
A19: x = g1 and
A20: f . x = ((- a) + g1) + b by A2, A3, A14;
(- a) + g1 = (- a) + g2 by A16, A20, A18, Th6;
hence x = y by A19, A17, Th6; :: thesis: verum

end;

hence a + H,H + b are_equipotent by A2, A4, WELLORD2:def 4; :: thesis: verum