let X, Y be non empty set ; :: thesis: for f being Function of X,Y st f is bijective holds

X,Y are_equipotent

let f be Function of X,Y; :: thesis: ( f is bijective implies X,Y are_equipotent )

assume A1: f is bijective ; :: thesis: X,Y are_equipotent

take h = f; :: according to TARSKI:def 6 :: thesis: ( ( for b_{1} being object holds

( not b_{1} in X or ex b_{2} being object st

( b_{2} in Y & [b_{1},b_{2}] in h ) ) ) & ( for b_{1} being object holds

( not b_{1} in Y or ex b_{2} being object st

( b_{2} in X & [b_{2},b_{1}] in h ) ) ) & ( for b_{1}, b_{2}, b_{3}, b_{4} being object holds

( not [b_{1},b_{2}] in h or not [b_{3},b_{4}] in h or ( ( not b_{1} = b_{3} or b_{2} = b_{4} ) & ( not b_{2} = b_{4} or b_{1} = b_{3} ) ) ) ) )

A2: ( h is one-to-one & h is onto ) by A1, FUNCT_2:def 4;

then A3: rng h = Y by FUNCT_2:def 3;

assume that

A6: [x,y] in h and

A7: [z,u] in h ; :: thesis: ( ( not x = z or y = u ) & ( not y = u or x = z ) )

A8: ( z in dom h & u = h . z ) by A7, FUNCT_1:1;

( x in dom h & y = h . x ) by A6, FUNCT_1:1;

hence ( ( not x = z or y = u ) & ( not y = u or x = z ) ) by A2, A8; :: thesis: verum

X,Y are_equipotent

let f be Function of X,Y; :: thesis: ( f is bijective implies X,Y are_equipotent )

assume A1: f is bijective ; :: thesis: X,Y are_equipotent

take h = f; :: according to TARSKI:def 6 :: thesis: ( ( for b

( not b

( b

( not b

( b

( not [b

A2: ( h is one-to-one & h is onto ) by A1, FUNCT_2:def 4;

then A3: rng h = Y by FUNCT_2:def 3;

hereby :: thesis: ( ( for b_{1} being object holds

( not b_{1} in Y or ex b_{2} being object st

( b_{2} in X & [b_{2},b_{1}] in h ) ) ) & ( for b_{1}, b_{2}, b_{3}, b_{4} being object holds

( not [b_{1},b_{2}] in h or not [b_{3},b_{4}] in h or ( ( not b_{1} = b_{3} or b_{2} = b_{4} ) & ( not b_{2} = b_{4} or b_{1} = b_{3} ) ) ) ) )

( not b

( b

( not [b

let x be object ; :: thesis: ( x in X implies ex y being object st

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

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

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

reconsider y = h . x as object ;

take y = y; :: thesis: ( y in Y & [x,y] in h )

thus y in Y by A3, A4, FUNCT_2:4; :: thesis: [x,y] in h

x in dom h by A4, FUNCT_2:def 1;

hence [x,y] in h by FUNCT_1:1; :: thesis: verum

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

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

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

reconsider y = h . x as object ;

take y = y; :: thesis: ( y in Y & [x,y] in h )

thus y in Y by A3, A4, FUNCT_2:4; :: thesis: [x,y] in h

x in dom h by A4, FUNCT_2:def 1;

hence [x,y] in h by FUNCT_1:1; :: thesis: verum

hereby :: thesis: for b_{1}, b_{2}, b_{3}, b_{4} being object holds

( not [b_{1},b_{2}] in h or not [b_{3},b_{4}] in h or ( ( not b_{1} = b_{3} or b_{2} = b_{4} ) & ( not b_{2} = b_{4} or b_{1} = b_{3} ) ) )

let x, y, z, u be object ; :: thesis: ( not [x,y] in h or not [z,u] in h or ( ( not x = z or y = u ) & ( not y = u or x = z ) ) )( not [b

let y be object ; :: thesis: ( y in Y implies ex x being object st

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

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

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

then consider x being object such that

A5: ( x in dom h & y = h . x ) by A3, FUNCT_1:def 3;

reconsider x = x as object ;

take x = x; :: thesis: ( x in X & [x,y] in h )

thus ( x in X & [x,y] in h ) by A5, FUNCT_1:1; :: thesis: verum

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

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

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

then consider x being object such that

A5: ( x in dom h & y = h . x ) by A3, FUNCT_1:def 3;

reconsider x = x as object ;

take x = x; :: thesis: ( x in X & [x,y] in h )

thus ( x in X & [x,y] in h ) by A5, FUNCT_1:1; :: thesis: verum

assume that

A6: [x,y] in h and

A7: [z,u] in h ; :: thesis: ( ( not x = z or y = u ) & ( not y = u or x = z ) )

A8: ( z in dom h & u = h . z ) by A7, FUNCT_1:1;

( x in dom h & y = h . x ) by A6, FUNCT_1:1;

hence ( ( not x = z or y = u ) & ( not y = u or x = z ) ) by A2, A8; :: thesis: verum