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 Th10;

hence X,Y are_equipotent by Th11; :: thesis: verum

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 Th10;

hence X,Y are_equipotent by Th11; :: thesis: verum