let Y be set ; :: thesis: for f being Function st rng f c= Y holds
f is Function of (dom f),Y
let f be Function; :: thesis: ( rng f c= Y implies f is Function of (dom f),Y )
assume rng f c= Y ; :: thesis: f is Function of (dom f),Y
then reconsider R = f as Relation of (dom f),Y by RELSET_1:4;
R is quasi_total

proof

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

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

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

end;

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

hence R = {} ; :: thesis: verum

end;

end;

end;

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