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;
( Y = {} or Y <> {} ) ;
then R is quasi_total by Def1;
hence f is Function of (dom f),Y ; :: thesis: verum