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 )

proof

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

proof

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;

then reconsider F = Z /\ [:X,Y:] as Function by FUNCT_1:def 1;
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

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;

thus dom f c= X :: according to XBOOLE_0:def 10 :: thesis: ( X c= dom f & rng f = Y )

proof

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;

thus X c= dom f :: thesis: rng f = Y

proof

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;

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

proof

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;

thus Y c= rng f :: 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;

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: 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

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;

thus for y being object st y in Y holds
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 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;

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

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