let X, Y be non empty set ; for f being Function of X,Y st f is bijective holds
X,Y are_equipotent
let f be Function of X,Y; ( f is bijective implies X,Y are_equipotent )
assume A1:
f is bijective
; X,Y are_equipotent
take h = f; TARSKI:def 6 ( ( for b1 being object holds
( not b1 in X or ex b2 being object st
( b2 in Y & [b1,b2] in h ) ) ) & ( for b1 being object holds
( not b1 in Y or ex b2 being object st
( b2 in X & [b2,b1] in h ) ) ) & ( for b1, b2, b3, b4 being object holds
( not [b1,b2] in h or not [b3,b4] in h or ( ( not b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) ) ) )
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 ( ( for b1 being object holds
( not b1 in Y or ex b2 being object st
( b2 in X & [b2,b1] in h ) ) ) & ( for b1, b2, b3, b4 being object holds
( not [b1,b2] in h or not [b3,b4] in h or ( ( not b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) ) ) )
end;
hereby for b1, b2, b3, b4 being object holds
( not [b1,b2] in h or not [b3,b4] in h or ( ( not b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) )
end;
let x, y, z, u be object ; ( 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
; ( ( 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; verum