let X, Y be set ; :: thesis: for f being Function st dom f = X & ( for x being set 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 set 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 set st x in X holds
f . x in Y ; :: thesis: f is Function of X,Y
rng f c= Y

proof

let y be set ; :: 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 set 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;
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 that A3: Y = {} and
dom f <> {} ; :: thesis: R = {}

thus R = {} by A3; :: thesis: verum

end;

end;

end;

hence f is Function of X,Y by A1; :: thesis: verum