let X, Y, Z be set ; :: thesis: for f being Function of X,Y st ( Y = {} implies X = {} ) & rng f c= Z holds
f is Function of X,Z
let f be Function of X,Y; :: thesis: ( ( Y = {} implies X = {} ) & rng f c= Z implies f is Function of X,Z )
assume ( Y <> {} or X = {} ) ; :: thesis: ( not rng f c= Z or f is Function of X,Z )
then A1: dom f = X by Def1;
assume A2: rng f c= Z ; :: thesis: f is Function of X,Z

now

assume Z = {} ; :: thesis: X = {}
then rng f = {} by A2;
hence X = {} by A1, RELAT_1:65; :: thesis: verum

end;

hence f is Function of X,Z by A1, A2, Def1, RELSET_1:11; :: thesis: verum