let G be Group; 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; for H being Subgroup of G holds a * H,H * b are_equipotent
let H be Subgroup of G; a * H,H * b are_equipotent
defpred S1[ 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 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 =
((a ") * g) * b as
set ;
take
y
;
S1[x,y]
take
g
;
( x = g & y = ((a ") * g) * b )
thus
(
x = g &
y = ((a ") * g) * b )
;
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 = H * b
f is one-to-one
proof
let x,
y be
object ;
FUNCT_1:def 4 ( 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
;
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, GROUP_1:6;
hence
x = y
by A19, A17, GROUP_1:6;
verum
end;
hence
a * H,H * b are_equipotent
by A2, A4, WELLORD2:def 4; verum