let x, X be set ; :: thesis: ( x in Funcs X,X implies x is Function of X,X )
assume x in Funcs X,X ; :: thesis: x is Function of X,X
then ex f being Function st
( x = f & dom f = X & rng f c= X ) by FUNCT_2:def 2;
hence x is Function of X,X by FUNCT_2:4; :: thesis: verum