theorem :: RFUNCT_3:24

for D being non empty set
for G1, G2, G3 being Element of PFuncs (D,REAL) holds Sum <*G1,G2,G3*> = (G1 + G2) + G3