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₁ being object holds
( not b₁ in X or ex b₂ being object st
( b₂ in Y & [b₁,b₂] in h ) ) ) & ( for b₁ being object holds
( not b₁ in Y or ex b₂ being object st
( b₂ in X & [b₂,b₁] in h ) ) ) & ( for b₁, b₂, b₃, b₄ being object 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₃ ) ) ) ) )
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₁ being object holds
( not b₁ in Y or ex b₂ being object st
( b₂ in X & [b₂,b₁] in h ) ) ) & ( for b₁, b₂, b₃, b₄ being object 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 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;

hereby :: thesis: for b₁, b₂, b₃, b₄ being object 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 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;

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