let G be Group; :: thesis: for A being non empty Subset of G
for x being Element of G holds card A = card (A * x)
let A be non empty Subset of G; :: thesis: for x being Element of G holds card A = card (A * x)
let x be Element of G; :: thesis: card A = card (A * x)
set B = A * x;
( not A is empty & not A * x is empty )

proof

set a = the Element of A;
the Element of A * x in A * x by GROUP_2:28;
hence ( not A is empty & not A * x is empty ) ; :: thesis: verum

end;

then reconsider B = A * x as non empty Subset of G ;
deffunc H₁( Element of G) -> Element of the carrier of G = $1 * x;
consider f being Function of A, the carrier of G such that
A1: for a being Element of A holds f . a = H₁(a) from FUNCT_2:sch 4();
A2: B c= rng f

proof

let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in B or s in rng f )
assume s in B ; :: thesis: s in rng f
then consider a being Element of G such that
A3: ( s = a * x & a in A ) by GROUP_2:28;
ex x being set st
( x in dom f & s = f . x )

proof

take a ; :: thesis: ( a in dom f & s = f . a )
thus ( a in dom f & s = f . a ) by A1, A3, FUNCT_2:def 1; :: thesis: verum

end;

hence s in rng f by FUNCT_1:def 3; :: thesis: verum

end;

A4: dom f = A by FUNCT_2:def 1;
A5: rng f c= B

proof

let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in rng f or s in B )
assume s in rng f ; :: thesis: s in B
then consider a being object such that
A6: a in A and
A7: s = f . a by A4, FUNCT_1:def 3;
reconsider a = a as Element of A by A6;
s = H₁(a) by A1, A7;
hence s in B by GROUP_2:28; :: thesis: verum

end;

then reconsider f = f as Function of A,B by A4, FUNCT_2:2;
A8: for a, b being Element of A st f . a = f . b holds
a = b

proof

let a, b be Element of A; :: thesis: ( f . a = f . b implies a = b )
assume f . a = f . b ; :: thesis: a = b
then H₁(a) = f . b by A1;
then a * x = b * x by A1;
hence a = b by GROUP_1:6; :: thesis: verum

end;

A,B are_equipotent

proof

take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & dom f = A & rng f = B )
thus ( f is one-to-one & dom f = A & rng f = B ) by A5, A2, A8, FUNCT_2:def 1, GROUP_6:1, XBOOLE_0:def 10; :: thesis: verum

end;

hence card A = card (A * x) by CARD_1:5; :: thesis: verum