:: deftheorem defines Sum RFUNCT_3:def 5 :
for D being non empty set
for f being FinSequence of PFuncs (D,REAL) holds Sum f = (addpfunc D) $$ f;