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_{1}[ 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_{1}[x,y]

A2: dom f = a * H and

A3: for x being object st x in a * H holds

S_{1}[x,f . x]
from CLASSES1:sch 1(A1);

A4: rng f = H * b

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

( $1 = g1 & $2 = ((a ") * g1) * b );

A1: for x being object st x in a * H holds

ex y being object st S

proof

consider f being Function such that
let x be object ; :: thesis: ( x in a * H implies ex y being object st S_{1}[x,y] )

assume x in a * H ; :: thesis: ex y being object st S_{1}[x,y]

then reconsider g = x as Element of G ;

reconsider y = ((a ") * g) * b as set ;

take y ; :: thesis: S_{1}[x,y]

take g ; :: thesis: ( x = g & y = ((a ") * g) * b )

thus ( x = g & y = ((a ") * g) * b ) ; :: thesis: verum

end;assume x in a * H ; :: thesis: ex y being object st S

then reconsider g = x as Element of G ;

reconsider y = ((a ") * g) * b as set ;

take y ; :: thesis: S

take g ; :: thesis: ( x = g & y = ((a ") * g) * b )

thus ( x = g & y = ((a ") * g) * b ) ; :: thesis: verum

A2: dom f = a * H and

A3: for x being object st x in a * H holds

S

A4: rng f = H * b

proof

f is one-to-one
thus
rng f c= H * b
:: according to XBOOLE_0:def 10 :: thesis: H * b c= 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;

then ex g1 being Element of G st

( g1 = a * g & f . (a * g) = ((a ") * g1) * b ) by A2, A3;

then f . (a * g) = (((a ") * a) * g) * b by GROUP_1:def 3

.= ((1_ G) * g) * b by GROUP_1:def 5

.= x by A11, GROUP_1:def 4 ;

hence x in rng f by A13, FUNCT_1:def 3; :: thesis: verum

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H * b or x in rng f )
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, GROUP_1:def 3

.= ((1_ G) * g1) * b by GROUP_1:def 5

.= g1 * b by GROUP_1:def 4 ;

hence x in H * b by A10, Th104; :: thesis: verum

end;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, GROUP_1:def 3

.= ((1_ G) * g1) * b by GROUP_1:def 5

.= g1 * b by GROUP_1:def 4 ;

hence x in H * b by A10, Th104; :: thesis: verum

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;

then ex g1 being Element of G st

( g1 = a * g & f . (a * g) = ((a ") * g1) * b ) by A2, A3;

then f . (a * g) = (((a ") * a) * g) * b by GROUP_1:def 3

.= ((1_ G) * g) * b by GROUP_1:def 5

.= x by A11, GROUP_1:def 4 ;

hence x in rng f by A13, FUNCT_1:def 3; :: thesis: verum

proof

hence
a * H,H * b are_equipotent
by A2, A4, WELLORD2:def 4; :: thesis: verum
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, GROUP_1:6;

hence x = y by A19, A17, GROUP_1:6; :: thesis: verum

end;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, GROUP_1:6;

hence x = y by A19, A17, GROUP_1:6; :: thesis: verum