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 )

deffunc H_{1}( 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_{1}(a)
from FUNCT_2:sch 4();

A2: dom f = A by FUNCT_2:def 1;

A3: rng f c= B

deffunc H_{2}( 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 = H_{2}(b)
from FUNCT_2:sch 4();

A10: dom g = B by FUNCT_2:def 1;

rng g c= A

A16: for a, b being Element of A st f . a = f . b holds

a = b

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

then reconsider B = ((x ") * A) * x as non empty Subset of G ;
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;((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

deffunc H

consider f being Function of A, the carrier of G such that

A1: for a being Element of A holds f . a = H

A2: dom f = A by FUNCT_2:def 1;

A3: rng f c= B

proof

A6:
B c= rng f
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 A2, FUNCT_1:def 3;

reconsider a = a as Element of A by A4;

s = H_{1}(a)
by A1, A5;

hence s in B by Th15; :: thesis: verum

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

reconsider a = a as Element of A by A4;

s = H

hence s in B by Th15; :: thesis: verum

proof

reconsider f = f as Function of A,B by A2, A3, FUNCT_2:2;
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 )

end;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

hence
s in rng f
by FUNCT_1:def 3; :: thesis: verum
take
a
; :: thesis: ( a in dom f & s = f . a )

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

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

deffunc H

consider g being Function of B, the carrier of G such that

A9: for b being Element of B holds g . b = H

A10: dom g = B by FUNCT_2:def 1;

rng g c= A

proof

then reconsider g = g as Function of B,A by A10, FUNCT_2:2;
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 A10, FUNCT_1:def 3;

reconsider a = a as Element of B by A11;

A13: s = H_{2}(a)
by A9, A12;

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 A13, A14, GROUP_1:def 3

.= (((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;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 A10, FUNCT_1:def 3;

reconsider a = a as Element of B by A11;

A13: s = H

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 A13, A14, GROUP_1:def 3

.= (((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

A16: for a, b being Element of A st f . a = f . b holds

a = b

proof

A,B are_equipotent
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 A9, A18

.= ((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 A9, A19

.= ((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 A17, A20; :: thesis: verum

end;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 A9, A18

.= ((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 A9, A19

.= ((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 A17, A20; :: thesis: verum

proof

hence
card A = card (((x ") * A) * x)
by CARD_1:5; :: thesis: verum
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, A6, A16, FUNCT_2:def 1, GROUP_6:1, XBOOLE_0:def 10; :: thesis: verum

end;thus ( f is one-to-one & dom f = A & rng f = B ) by A3, A6, A16, FUNCT_2:def 1, GROUP_6:1, XBOOLE_0:def 10; :: thesis: verum