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:11;
R is quasi_total

proof

per cases not ( rng f = {} & not dom f = {} & not ( rng f = {} & dom f <> {} ) ) ;
:: according to FUNCT_2:def 1

case ( rng f = {} implies dom f = {} ) ; :: thesis: dom f = dom R

thus dom f = dom R ; :: thesis: verum

end;

case ( rng f = {} & dom f <> {} ) ; :: thesis: R = {}

hence R = {} ; :: thesis: verum

end;

end;

end;

hence f is Function of (dom f),(rng f) ; :: thesis: verum