let X, Y, Z be set ; 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; ( ( Y = {} implies X = {} ) & rng f c= Z implies f is Function of X,Z )
assume
( Y <> {} or X = {} )
; ( 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
; f is Function of X,Z
hence
f is Function of X,Z
by A1, A2, Def1, RELSET_1:4; verum