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