let X, Y be set ; :: thesis: for f being Function st dom f = X & ( for x being object st x in X holds
f . x in Y ) holds
f is Function of X,Y
let f be Function; :: thesis: ( dom f = X & ( for x being object st x in X holds
f . x in Y ) implies f is Function of X,Y )
assume that
A1: dom f = X and
A2: for x being object st x in X holds
f . x in Y ; :: thesis: f is Function of X,Y
rng f c= Y

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in Y )
assume y in rng f ; :: thesis: y in Y
then ex x being object st
( x in X & y = f . x ) by A1, FUNCT_1:def 3;
hence y in Y by A2; :: thesis: verum

end;

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 X,Y by A1; :: thesis: verum