let Y, X be non empty set ; :: thesis: ( ex f being Function of X,Y st f is bijective implies X,Y are_equipotent )
given h being Function of X,Y such that A1: h is bijective ; :: thesis: X,Y are_equipotent
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;
take h ; :: according to TARSKI:def 6 :: thesis: ( ( for b₁ being set holds
( not b₁ in X or ex b₂ being set st
( b₂ in Y & [b₁,b₂] in h ) ) ) & ( for b₁ being set holds
( not b₁ in Y or ex b₂ being set st
( b₂ in X & [b₂,b₁] in h ) ) ) & ( for b₁, b₂, b₃, b₄ being set holds
( not [b₁,b₂] in h or not [b₃,b₄] in h or ( ( not b₁ = b₃ or b₂ = b₄ ) & ( not b₂ = b₄ or b₁ = b₃ ) ) ) ) )

hereby :: thesis: ( ( for b₁ being set holds
( not b₁ in Y or ex b₂ being set st
( b₂ in X & [b₂,b₁] in h ) ) ) & ( for b₁, b₂, b₃, b₄ being set holds
( not [b₁,b₂] in h or not [b₃,b₄] in h or ( ( not b₁ = b₃ or b₂ = b₄ ) & ( not b₂ = b₄ or b₁ = b₃ ) ) ) ) )

let x be set ; :: thesis: ( x in X implies ex y being set st
( y in Y & [x,y] in h ) )
assume A4: x in X ; :: thesis: ex y being set st
( y in Y & [x,y] in h )
then A5: x in dom h by FUNCT_2:def 1;
take y = h . x; :: thesis: ( y in Y & [x,y] in h )
thus y in Y by A3, A4, FUNCT_2:6; :: thesis: [x,y] in h
thus [x,y] in h by A5, FUNCT_1:8; :: thesis: verum

end;

hereby :: thesis: for b₁, b₂, b₃, b₄ being set holds
( not [b₁,b₂] in h or not [b₃,b₄] in h or ( ( not b₁ = b₃ or b₂ = b₄ ) & ( not b₂ = b₄ or b₁ = b₃ ) ) )

let y be set ; :: thesis: ( y in Y implies ex x being set st
( x in X & [x,y] in h ) )
assume y in Y ; :: thesis: ex x being set st
( x in X & [x,y] in h )
then consider x being set such that
A6: ( x in dom h & y = h . x ) by A3, FUNCT_1:def 5;
take x = x; :: thesis: ( x in X & [x,y] in h )
thus ( x in X & [x,y] in h ) by A6, FUNCT_1:8; :: thesis: verum

end;

let x, y, z, u be set ; :: 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 ) ) )
assume ( [x,y] in h & [z,u] in h ) ; :: thesis: ( ( not x = z or y = u ) & ( not y = u or x = z ) )
then ( x in dom h & y = h . x & z in dom h & u = h . z ) by FUNCT_1:8;
hence ( ( not x = z or y = u ) & ( not y = u or x = z ) ) by A2, FUNCT_1:def 8; :: thesis: verum