theorem :: RFUNCT_3:22

for D being non empty set
for f being FinSequence of PFuncs (D,REAL)
for G being Element of PFuncs (D,REAL) holds Sum (<*G*> ^ f) = G + (Sum f)