let X, Y be non empty set ; :: thesis: for f being Function of X,Y
for g being Function of Y,X st f is one-to-one & g is one-to-one holds
X,Y are_equipotent
let f be Function of X,Y; :: thesis: for g being Function of Y,X st f is one-to-one & g is one-to-one holds
X,Y are_equipotent
let g be Function of Y,X; :: thesis: ( f is one-to-one & g is one-to-one implies X,Y are_equipotent )
assume ( f is one-to-one & g is one-to-one ) ; :: thesis: X,Y are_equipotent
then ex h being Function of X,Y st h is bijective by Th12;
hence X,Y are_equipotent by Th13; :: thesis: verum