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

assume X,Y are_equipotent ; :: thesis:
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

let x, y, z be object ; :: thesis:
assume ( [x,y] in Z /\ [:X,Y:] & [x,z] in Z /\ [:X,Y:] ) ; :: thesis:
then ( [x,y] in Z & [x,z] in Z ) by XBOOLE_0:def 4;
hence y = z by A3; :: thesis:

end;

then reconsider F = Z /\ [:X,Y:] as Function by FUNCT_1:def 1;
take f = F; :: thesis:
thus f is one-to-one :: thesis:

proof

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A4: x in dom f and
A5: y in dom f and
A6: f . x = f . y ; :: thesis:
[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:

end;

thus dom f c= X :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in dom f ; :: thesis:
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:

end;

thus X c= dom f :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A8: x in X ; :: thesis:
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:

end;

thus rng f c= Y :: according to XBOOLE_0:def 10 :: thesis:

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng f ; :: thesis:
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:

end;

thus Y c= rng f :: thesis:

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A12: y in Y ; :: thesis:
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:

end;

( ex f being Function st
( 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

given f being Function such that A15: f is one-to-one and
A16: dom f = X and
A17: rng f = Y ; :: thesis:
take Z = f; :: thesis:
thus for x being object st x in X holds
ex y being object st
( y in Y & [x,y] in Z ) :: thesis:

proof

let x be object ; :: thesis:
assume A18: x in X ; :: thesis:
take f . x ; :: thesis:
thus f . x in Y by A16, A17, A18, FUNCT_1:def 3; :: thesis:
thus [x,(f . x)] in Z by A16, A18, FUNCT_1:1; :: thesis:

end;

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

proof

let y be object ; :: thesis:
assume A19: y in Y ; :: thesis:
take (f ") . y ; :: thesis:
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:
y = f . ((f ") . y) by A15, A17, A19, FUNCT_1:35;
hence [((f ") . y),y] in Z by A22, A21, FUNCT_1:1; :: thesis:

end;

let x, y, z, u be object ; :: thesis:
assume A23: ( [x,y] in Z & [z,u] in Z ) ; :: thesis:
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:

end;

hence ( ex f being Function st
( f is one-to-one & dom f = X & rng f = Y ) implies X,Y are_equipotent ) ; :: thesis: