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

consider a being Element of A;
((x " ) * 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 H₁( 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 = H₁(a) from FUNCT_2:sch 4();
A2: dom f = A by FUNCT_2:def 1;
A3: rng f = B

proof

A4: rng f c= B

proof

let s be set ; :: 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 set such that
A5: ( a in A & s = f . a ) by A2, FUNCT_1:def 5;
reconsider a = a as Element of A by A5;
s = H₁(a) by A1, A5;
hence s in B by Th15; :: thesis: verum

end;

B c= rng f

proof

let s be set ; :: 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
A6: ( s = ((x " ) * a) * x & a in A ) by Th15;
ex x being Element of G st
( x in dom f & s = f . x )

proof

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

end;

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

end;

hence rng f = B by A4, XBOOLE_0:def 10; :: thesis: verum

end;

then reconsider f = f as Function of A,B by A2, FUNCT_2:4;
deffunc H₂( Element of G) -> Element of the carrier of G = (x * $1) * (x " );
consider g being Function of B,the carrier of G such that
A7: for b being Element of B holds g . b = H₂(b) from FUNCT_2:sch 4();
A8: dom g = B by FUNCT_2:def 1;
rng g = A

proof

A9: rng g c= A

proof

let s be set ; :: 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 set such that
A10: ( a in B & s = g . a ) by A8, FUNCT_1:def 5;
reconsider a = a as Element of B by A10;
A11: s = H₂(a) by A7, A10;
consider c being Element of G such that
A12: ( a = ((x " ) * c) * x & c in A ) by Th15;
s = ((x * ((x " ) * c)) * x) * (x " ) by A11, A12, GROUP_1:def 4
.= (((x * (x " )) * c) * x) * (x " ) by GROUP_1:def 4
.= ((x * (x " )) * c) * (x * (x " )) by GROUP_1:def 4
.= ((1_ G) * c) * (x * (x " )) by GROUP_1:def 6
.= ((1_ G) * c) * (1_ G) by GROUP_1:def 6
.= (1_ G) * c by GROUP_1:def 5
.= c by GROUP_1:def 5 ;
hence s in A by A12; :: thesis: verum

end;

A c= rng g

proof

let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in A or s in rng g )
assume s in A ; :: thesis: s in rng g
then reconsider s = s as Element of A ;
consider b being Element of G such that
A13: b = ((x " ) * s) * x ;
A14: b in B by A13, Th15;
ex u being set st
( u in dom g & s = g . u )

proof

take u = b; :: thesis: ( u in dom g & s = g . u )
g . u = (x * (((x " ) * s) * x)) * (x " ) by A7, A13, A14
.= ((x * ((x " ) * s)) * x) * (x " ) by GROUP_1:def 4
.= (((x * (x " )) * s) * x) * (x " ) by GROUP_1:def 4
.= ((x * (x " )) * s) * (x * (x " )) by GROUP_1:def 4
.= ((1_ G) * s) * (x * (x " )) by GROUP_1:def 6
.= ((1_ G) * s) * (1_ G) by GROUP_1:def 6
.= (1_ G) * s by GROUP_1:def 5
.= s by GROUP_1:def 5 ;
hence ( u in dom g & s = g . u ) by A14, FUNCT_2:def 1; :: thesis: verum

end;

hence s in rng g by FUNCT_1:def 5; :: thesis: verum

end;

hence rng g = A by A9, XBOOLE_0:def 10; :: thesis: verum

end;

then reconsider g = g as Function of B,A by A8, FUNCT_2:4;
A15: 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 A16: f . a = f . b ; :: thesis: a = b
A17: ((x " ) * a) * x in B by Th15;
A18: ((x " ) * b) * x in B by Th15;
A19: g . (f . a) = g . (((x " ) * a) * x) by A1
.= (x * (((x " ) * a) * x)) * (x " ) by A7, A17
.= ((x * ((x " ) * a)) * x) * (x " ) by GROUP_1:def 4
.= (((x * (x " )) * a) * x) * (x " ) by GROUP_1:def 4
.= ((x * (x " )) * a) * (x * (x " )) by GROUP_1:def 4
.= ((1_ G) * a) * (x * (x " )) by GROUP_1:def 6
.= a * (x * (x " )) by GROUP_1:def 5
.= a * (1_ G) by GROUP_1:def 6
.= a by GROUP_1:def 5 ;
g . (f . b) = g . (((x " ) * b) * x) by A1
.= (x * (((x " ) * b) * x)) * (x " ) by A7, A18
.= ((x * ((x " ) * b)) * x) * (x " ) by GROUP_1:def 4
.= (((x * (x " )) * b) * x) * (x " ) by GROUP_1:def 4
.= ((x * (x " )) * b) * (x * (x " )) by GROUP_1:def 4
.= ((1_ G) * b) * (x * (x " )) by GROUP_1:def 6
.= b * (x * (x " )) by GROUP_1:def 5
.= b * (1_ G) by GROUP_1:def 6
.= b by GROUP_1:def 5 ;
hence a = b by A16, A19; :: 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 A3, A15, FUNCT_2:def 1, GROUP_6:1; :: thesis: verum

end;

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