let x, X be set ; :: thesis: ( x is Element of (GPFuncs X) iff x is PartFunc of X,X )
H₁( GPFuncs X) = PFuncs (X,X) by Def37;
hence ( x is Element of (GPFuncs X) iff x is PartFunc of X,X ) by PARTFUN1:45, PARTFUN1:46; :: thesis: verum