thus
( X,Y are_equipotent implies ex f being Function st

( f is one-to-one & dom f = X & rng f = Y ) ) :: thesis: ( ex f being Function st

( f is one-to-one & dom f = X & rng f = Y ) implies X,Y are_equipotent )

( f is one-to-one & dom f = X & rng f = Y ) implies ex Z being set st

( ( for x being object st x in X holds

ex y being object st

( y in Y & [x,y] in Z ) ) & ( for y being object st y in Y holds

ex x being object st

( x in X & [x,y] in Z ) ) & ( for x, y, z, u being object st [x,y] in Z & [z,u] in Z holds

( x = z iff y = u ) ) ) )

( f is one-to-one & dom f = X & rng f = Y ) implies X,Y are_equipotent ) ; :: thesis: verum

( f is one-to-one & dom f = X & rng f = Y ) ) :: thesis: ( ex f being Function st

( f is one-to-one & dom f = X & rng f = Y ) implies X,Y are_equipotent )

proof

( ex f being Function st
assume
X,Y are_equipotent
; :: thesis: ex f being Function st

( f is one-to-one & dom f = X & rng f = Y )

then consider Z being set such that

A1: for x being object st x in X holds

ex y being object st

( y in Y & [x,y] in Z ) and

A2: for y being object st y in Y holds

ex x being object st

( x in X & [x,y] in Z ) and

A3: for x, y, z, u being object st [x,y] in Z & [z,u] in Z holds

( x = z iff y = u ) ;

set F = Z /\ [:X,Y:];

for x, y, z being object st [x,y] in Z /\ [:X,Y:] & [x,z] in Z /\ [:X,Y:] holds

y = z

take f = F; :: thesis: ( f is one-to-one & dom f = X & rng f = Y )

thus f is one-to-one :: thesis: ( dom f = X & rng f = Y )

end;( f is one-to-one & dom f = X & rng f = Y )

then consider Z being set such that

A1: for x being object st x in X holds

ex y being object st

( y in Y & [x,y] in Z ) and

A2: for y being object st y in Y holds

ex x being object st

( x in X & [x,y] in Z ) and

A3: for x, y, z, u being object st [x,y] in Z & [z,u] in Z holds

( x = z iff y = u ) ;

set F = Z /\ [:X,Y:];

for x, y, z being object st [x,y] in Z /\ [:X,Y:] & [x,z] in Z /\ [:X,Y:] holds

y = z

proof

then reconsider F = Z /\ [:X,Y:] as Function by FUNCT_1:def 1;
let x, y, z be object ; :: thesis: ( [x,y] in Z /\ [:X,Y:] & [x,z] in Z /\ [:X,Y:] implies y = z )

assume ( [x,y] in Z /\ [:X,Y:] & [x,z] in Z /\ [:X,Y:] ) ; :: thesis: y = z

then ( [x,y] in Z & [x,z] in Z ) by XBOOLE_0:def 4;

hence y = z by A3; :: thesis: verum

end;assume ( [x,y] in Z /\ [:X,Y:] & [x,z] in Z /\ [:X,Y:] ) ; :: thesis: y = z

then ( [x,y] in Z & [x,z] in Z ) by XBOOLE_0:def 4;

hence y = z by A3; :: thesis: verum

take f = F; :: thesis: ( f is one-to-one & dom f = X & rng f = Y )

thus f is one-to-one :: thesis: ( dom f = X & rng f = Y )

proof

thus
dom f c= X
:: according to XBOOLE_0:def 10 :: thesis: ( X c= dom f & rng f = Y )
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

A4: x in dom f and

A5: y in dom f and

A6: f . x = f . y ; :: thesis: x = y

[y,(f . y)] in f by A5, FUNCT_1:1;

then A7: [y,(f . y)] in Z by XBOOLE_0:def 4;

[x,(f . x)] in f by A4, FUNCT_1:1;

then [x,(f . x)] in Z by XBOOLE_0:def 4;

hence x = y by A3, A6, A7; :: thesis: verum

end;assume that

A4: x in dom f and

A5: y in dom f and

A6: f . x = f . y ; :: thesis: x = y

[y,(f . y)] in f by A5, FUNCT_1:1;

then A7: [y,(f . y)] in Z by XBOOLE_0:def 4;

[x,(f . x)] in f by A4, FUNCT_1:1;

then [x,(f . x)] in Z by XBOOLE_0:def 4;

hence x = y by A3, A6, A7; :: thesis: verum

proof

thus
X c= dom f
:: thesis: rng f = Y
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in X )

assume x in dom f ; :: thesis: x in X

then [x,(f . x)] in f by FUNCT_1:1;

then [x,(f . x)] in [:X,Y:] by XBOOLE_0:def 4;

hence x in X by ZFMISC_1:87; :: thesis: verum

end;assume x in dom f ; :: thesis: x in X

then [x,(f . x)] in f by FUNCT_1:1;

then [x,(f . x)] in [:X,Y:] by XBOOLE_0:def 4;

hence x in X by ZFMISC_1:87; :: thesis: verum

proof

thus
rng f c= Y
:: according to XBOOLE_0:def 10 :: thesis: Y c= rng f
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in dom f )

assume A8: x in X ; :: thesis: x in dom f

then consider y being object such that

A9: y in Y and

A10: [x,y] in Z by A1;

[x,y] in [:X,Y:] by A8, A9, ZFMISC_1:87;

then [x,y] in f by A10, XBOOLE_0:def 4;

hence x in dom f by FUNCT_1:1; :: thesis: verum

end;assume A8: x in X ; :: thesis: x in dom f

then consider y being object such that

A9: y in Y and

A10: [x,y] in Z by A1;

[x,y] in [:X,Y:] by A8, A9, ZFMISC_1:87;

then [x,y] in f by A10, XBOOLE_0:def 4;

hence x in dom f by FUNCT_1:1; :: thesis: verum

proof

thus
Y c= rng f
:: thesis: verum
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in Y )

assume y in rng f ; :: thesis: y in Y

then consider x being object such that

A11: ( x in dom f & y = f . x ) by FUNCT_1:def 3;

[x,y] in f by A11, FUNCT_1:1;

then [x,y] in [:X,Y:] by XBOOLE_0:def 4;

hence y in Y by ZFMISC_1:87; :: thesis: verum

end;assume y in rng f ; :: thesis: y in Y

then consider x being object such that

A11: ( x in dom f & y = f . x ) by FUNCT_1:def 3;

[x,y] in f by A11, FUNCT_1:1;

then [x,y] in [:X,Y:] by XBOOLE_0:def 4;

hence y in Y by ZFMISC_1:87; :: thesis: verum

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in rng f )

assume A12: y in Y ; :: thesis: y in rng f

then consider x being object such that

A13: x in X and

A14: [x,y] in Z by A2;

[x,y] in [:X,Y:] by A12, A13, ZFMISC_1:87;

then [x,y] in f by A14, XBOOLE_0:def 4;

then ( x in dom f & y = f . x ) by FUNCT_1:1;

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

end;assume A12: y in Y ; :: thesis: y in rng f

then consider x being object such that

A13: x in X and

A14: [x,y] in Z by A2;

[x,y] in [:X,Y:] by A12, A13, ZFMISC_1:87;

then [x,y] in f by A14, XBOOLE_0:def 4;

then ( x in dom f & y = f . x ) by FUNCT_1:1;

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

( f is one-to-one & dom f = X & rng f = Y ) implies ex Z being set st

( ( for x being object st x in X holds

ex y being object st

( y in Y & [x,y] in Z ) ) & ( for y being object st y in Y holds

ex x being object st

( x in X & [x,y] in Z ) ) & ( for x, y, z, u being object st [x,y] in Z & [z,u] in Z holds

( x = z iff y = u ) ) ) )

proof

hence
( ex f being Function st
given f being Function such that A15:
f is one-to-one
and

A16: dom f = X and

A17: rng f = Y ; :: thesis: ex Z being set st

( ( for x being object st x in X holds

ex y being object st

( y in Y & [x,y] in Z ) ) & ( for y being object st y in Y holds

ex x being object st

( x in X & [x,y] in Z ) ) & ( for x, y, z, u being object st [x,y] in Z & [z,u] in Z holds

( x = z iff y = u ) ) )

take Z = f; :: thesis: ( ( for x being object st x in X holds

ex y being object st

( y in Y & [x,y] in Z ) ) & ( for y being object st y in Y holds

ex x being object st

( x in X & [x,y] in Z ) ) & ( for x, y, z, u being object st [x,y] in Z & [z,u] in Z holds

( x = z iff y = u ) ) )

thus for x being object st x in X holds

ex y being object st

( y in Y & [x,y] in Z ) :: thesis: ( ( for y being object st y in Y holds

ex x being object st

( x in X & [x,y] in Z ) ) & ( for x, y, z, u being object st [x,y] in Z & [z,u] in Z holds

( x = z iff y = u ) ) )

ex x being object st

( x in X & [x,y] in Z ) :: thesis: for x, y, z, u being object st [x,y] in Z & [z,u] in Z holds

( x = z iff y = u )

assume A23: ( [x,y] in Z & [z,u] in Z ) ; :: thesis: ( x = z iff y = u )

then A24: ( x in dom f & z in dom f ) by FUNCT_1:1;

( y = f . x & u = f . z ) by A23, FUNCT_1:1;

hence ( x = z iff y = u ) by A15, A24; :: thesis: verum

end;A16: dom f = X and

A17: rng f = Y ; :: thesis: ex Z being set st

( ( for x being object st x in X holds

ex y being object st

( y in Y & [x,y] in Z ) ) & ( for y being object st y in Y holds

ex x being object st

( x in X & [x,y] in Z ) ) & ( for x, y, z, u being object st [x,y] in Z & [z,u] in Z holds

( x = z iff y = u ) ) )

take Z = f; :: thesis: ( ( for x being object st x in X holds

ex y being object st

( y in Y & [x,y] in Z ) ) & ( for y being object st y in Y holds

ex x being object st

( x in X & [x,y] in Z ) ) & ( for x, y, z, u being object st [x,y] in Z & [z,u] in Z holds

( x = z iff y = u ) ) )

thus for x being object st x in X holds

ex y being object st

( y in Y & [x,y] in Z ) :: thesis: ( ( for y being object st y in Y holds

ex x being object st

( x in X & [x,y] in Z ) ) & ( for x, y, z, u being object st [x,y] in Z & [z,u] in Z holds

( x = z iff y = u ) ) )

proof

thus
for y being object st y in Y holds
let x be object ; :: thesis: ( x in X implies ex y being object st

( y in Y & [x,y] in Z ) )

assume A18: x in X ; :: thesis: ex y being object st

( y in Y & [x,y] in Z )

take f . x ; :: thesis: ( f . x in Y & [x,(f . x)] in Z )

thus f . x in Y by A16, A17, A18, FUNCT_1:def 3; :: thesis: [x,(f . x)] in Z

thus [x,(f . x)] in Z by A16, A18, FUNCT_1:1; :: thesis: verum

end;( y in Y & [x,y] in Z ) )

assume A18: x in X ; :: thesis: ex y being object st

( y in Y & [x,y] in Z )

take f . x ; :: thesis: ( f . x in Y & [x,(f . x)] in Z )

thus f . x in Y by A16, A17, A18, FUNCT_1:def 3; :: thesis: [x,(f . x)] in Z

thus [x,(f . x)] in Z by A16, A18, FUNCT_1:1; :: thesis: verum

ex x being object st

( x in X & [x,y] in Z ) :: thesis: for x, y, z, u being object st [x,y] in Z & [z,u] in Z holds

( x = z iff y = u )

proof

let x, y, z, u be object ; :: thesis: ( [x,y] in Z & [z,u] in Z implies ( x = z iff y = u ) )
let y be object ; :: thesis: ( y in Y implies ex x being object st

( x in X & [x,y] in Z ) )

assume A19: y in Y ; :: thesis: ex x being object st

( x in X & [x,y] in Z )

take (f ") . y ; :: thesis: ( (f ") . y in X & [((f ") . y),y] in Z )

A20: dom (f ") = rng f by A15, FUNCT_1:33;

then A21: (f ") . y in rng (f ") by A17, A19, FUNCT_1:def 3;

A22: rng (f ") = dom f by A15, FUNCT_1:33;

hence (f ") . y in X by A16, A17, A19, A20, FUNCT_1:def 3; :: thesis: [((f ") . y),y] in Z

y = f . ((f ") . y) by A15, A17, A19, FUNCT_1:35;

hence [((f ") . y),y] in Z by A22, A21, FUNCT_1:1; :: thesis: verum

end;( x in X & [x,y] in Z ) )

assume A19: y in Y ; :: thesis: ex x being object st

( x in X & [x,y] in Z )

take (f ") . y ; :: thesis: ( (f ") . y in X & [((f ") . y),y] in Z )

A20: dom (f ") = rng f by A15, FUNCT_1:33;

then A21: (f ") . y in rng (f ") by A17, A19, FUNCT_1:def 3;

A22: rng (f ") = dom f by A15, FUNCT_1:33;

hence (f ") . y in X by A16, A17, A19, A20, FUNCT_1:def 3; :: thesis: [((f ") . y),y] in Z

y = f . ((f ") . y) by A15, A17, A19, FUNCT_1:35;

hence [((f ") . y),y] in Z by A22, A21, FUNCT_1:1; :: thesis: verum

assume A23: ( [x,y] in Z & [z,u] in Z ) ; :: thesis: ( x = z iff y = u )

then A24: ( x in dom f & z in dom f ) by FUNCT_1:1;

( y = f . x & u = f . z ) by A23, FUNCT_1:1;

hence ( x = z iff y = u ) by A15, A24; :: thesis: verum

( f is one-to-one & dom f = X & rng f = Y ) implies X,Y are_equipotent ) ; :: thesis: verum