let X, Y be set ; :: thesis: for f being Function of X,Y st ( Y = {} implies X = {} ) holds
( f is one-to-one iff for x1, x2 being object st x1 in X & x2 in X & f . x1 = f . x2 holds
x1 = x2 )
let f be Function of X,Y; :: thesis: ( ( Y = {} implies X = {} ) implies ( f is one-to-one iff for x1, x2 being object st x1 in X & x2 in X & f . x1 = f . x2 holds
x1 = x2 ) )
assume ( Y = {} implies X = {} ) ; :: thesis: ( f is one-to-one iff for x1, x2 being object st x1 in X & x2 in X & f . x1 = f . x2 holds
x1 = x2 )
then dom f = X by Def1;
hence ( f is one-to-one iff for x1, x2 being object st x1 in X & x2 in X & f . x1 = f . x2 holds
x1 = x2 ) ; :: thesis: verum