let f be Function; :: thesis: f is Function of (dom f),(rng f)
reconsider R = f as Relation of (dom f),(rng f) by RELSET_1:4;
( rng R <> {} or rng R = {} ) ;
hence f is Function of (dom f),(rng f) by Def1; :: thesis: verum