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