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:11; :: thesis: verum