let G be Group; :: thesis: for A being non empty Subset of G
for x being Element of G holds card A = card (((x ") * A) * x)

let A be non empty Subset of G; :: thesis: for x being Element of G holds card A = card (((x ") * A) * x)
let x be Element of G; :: thesis: card A = card (((x ") * A) * x)
set B = ((x ") * A) * x;
( not A is empty & not ((x ") * A) * x is empty )
proof
set a = the Element of A;
((x ") * the Element of A) * x in ((x ") * A) * x by Th15;
hence ( not A is empty & not ((x ") * A) * x is empty ) ; :: thesis: verum
end;
then reconsider B = ((x ") * A) * x as non empty Subset of G ;
deffunc H1( Element of G) -> Element of the carrier of G = ((x ") * \$1) * x;
consider f being Function of A, the carrier of G such that
A1: for a being Element of A holds f . a = H1(a) from A2: dom f = A by FUNCT_2:def 1;
A3: 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
A4: a in A and
A5: s = f . a by ;
reconsider a = a as Element of A by A4;
s = H1(a) by A1, A5;
hence s in B by Th15; :: thesis: verum
end;
A6: 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
A7: s = ((x ") * a) * x and
A8: a in A by Th15;
ex x being Element of G 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 ; :: thesis: verum
end;
hence s in rng f by FUNCT_1:def 3; :: thesis: verum
end;
reconsider f = f as Function of A,B by ;
deffunc H2( Element of G) -> Element of the carrier of G = (x * \$1) * (x ");
consider g being Function of B, the carrier of G such that
A9: for b being Element of B holds g . b = H2(b) from A10: dom g = B by FUNCT_2:def 1;
rng g c= A
proof
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in rng g or s in A )
assume s in rng g ; :: thesis: s in A
then consider a being object such that
A11: a in B and
A12: s = g . a by ;
reconsider a = a as Element of B by A11;
A13: s = H2(a) by ;
consider c being Element of G such that
A14: a = ((x ") * c) * x and
A15: c in A by Th15;
s = ((x * ((x ") * c)) * x) * (x ") by
.= (((x * (x ")) * c) * x) * (x ") by GROUP_1:def 3
.= ((x * (x ")) * c) * (x * (x ")) by GROUP_1:def 3
.= ((1_ G) * c) * (x * (x ")) by GROUP_1:def 5
.= ((1_ G) * c) * (1_ G) by GROUP_1:def 5
.= (1_ G) * c by GROUP_1:def 4
.= c by GROUP_1:def 4 ;
hence s in A by A15; :: thesis: verum
end;
then reconsider g = g as Function of B,A by ;
A16: 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 A17: f . a = f . b ; :: thesis: a = b
A18: ((x ") * a) * x in B by Th15;
A19: ((x ") * b) * x in B by Th15;
A20: g . (f . a) = g . (((x ") * a) * x) by A1
.= (x * (((x ") * a) * x)) * (x ") by
.= ((x * ((x ") * a)) * x) * (x ") by GROUP_1:def 3
.= (((x * (x ")) * a) * x) * (x ") by GROUP_1:def 3
.= ((x * (x ")) * a) * (x * (x ")) by GROUP_1:def 3
.= ((1_ G) * a) * (x * (x ")) by GROUP_1:def 5
.= a * (x * (x ")) by GROUP_1:def 4
.= a * (1_ G) by GROUP_1:def 5
.= a by GROUP_1:def 4 ;
g . (f . b) = g . (((x ") * b) * x) by A1
.= (x * (((x ") * b) * x)) * (x ") by
.= ((x * ((x ") * b)) * x) * (x ") by GROUP_1:def 3
.= (((x * (x ")) * b) * x) * (x ") by GROUP_1:def 3
.= ((x * (x ")) * b) * (x * (x ")) by GROUP_1:def 3
.= ((1_ G) * b) * (x * (x ")) by GROUP_1:def 5
.= b * (x * (x ")) by GROUP_1:def 4
.= b * (1_ G) by GROUP_1:def 5
.= b by GROUP_1:def 4 ;
hence a = b by ; :: 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 ; :: thesis: verum
end;
hence card A = card (((x ") * A) * x) by CARD_1:5; :: thesis: verum