for A being non empty set
for f being Element of PFuncs (A,REAL) holds (addpfunc A) . (f,((multrealpfunc A) . ((- 1),f))) = (RealPFuncZero A) | (dom f)