let G be addGroup; for a, b being Element of G
for H being Subgroup of G holds a + H,b + H are_equipotent
let a, b be Element of G; for H being Subgroup of G holds a + H,b + H are_equipotent
let H be Subgroup of G; a + H,b + H are_equipotent
defpred S1[ object , object ] means ex g1 being Element of G st
( $1 = g1 & $2 = (b + (- a)) + g1 );
A1:
for x being object st x in a + H holds
ex y being object st S1[x,y]
proof
let x be
object ;
( x in a + H implies ex y being object st S1[x,y] )
assume
x in a + H
;
ex y being object st S1[x,y]
then reconsider g =
x as
Element of
G ;
reconsider y =
(b + (- a)) + g as
set ;
take
y
;
S1[x,y]
take
g
;
( x = g & y = (b + (- a)) + g )
thus
(
x = g &
y = (b + (- a)) + g )
;
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
S1[x,f . x]
from CLASSES1:sch 1(A1);
A4:
rng f = b + H
f is one-to-one
hence
a + H,b + H are_equipotent
by A2, A4, WELLORD2:def 4; verum