let x, X be set ; :: thesis: ( x is Element of (GFuncs X) iff x is Function of X,X )
H₁( GFuncs X) = Funcs (X,X) by Def40;
hence ( x is Element of (GFuncs X) iff x is Function of X,X ) by FUNCT_2:9, FUNCT_2:66; :: thesis: verum