let D be non empty set ; :: thesis: for f being FinSequence of PFuncs (D,REAL)
for G being Element of PFuncs (D,REAL) holds Sum (f ^ <*G*>) = (Sum f) + G
let f be FinSequence of PFuncs (D,REAL); :: thesis: for G being Element of PFuncs (D,REAL) holds Sum (f ^ <*G*>) = (Sum f) + G
let G be Element of PFuncs (D,REAL); :: thesis: Sum (f ^ <*G*>) = (Sum f) + G
set o = addpfunc D;
thus Sum (f ^ <*G*>) = (addpfunc D) . (((addpfunc D) $$ f),G) by Th18, FINSOP_1:4
.= (Sum f) + G by Def4 ; :: thesis: verum