let X, Y, f be set ; :: thesis: ( f in Funcs (X,Y) implies f is Function of X,Y )
assume f in Funcs (X,Y) ; :: thesis: f is Function of X,Y
then ( ( not Y = {} or not X <> {} ) & ex f9 being Function st
( f9 = f & dom f9 = X & rng f9 c= Y ) ) by Def2;
hence f is Function of X,Y by Def1, RELSET_1:4; :: thesis: verum