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 :: thesis: ( Z = {} implies X = {} )
assume Z = {} ; :: thesis: X = {}
then rng f = {} by A2;
hence X = {} by A1, RELAT_1:42; :: thesis: verum
end;
hence f is Function of X,Z by A1, A2, Def1, RELSET_1:4; :: thesis: verum