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