let G be Group; 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