H₁( GPFuncs X) = PFuncs X,X by Def37;
hence the multF of (GPFuncs X) is BinOp of (PFuncs X,X) ; :: thesis: verum