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 Th20, FINSOP_1:5
.= (Sum f) + G by Def4 ; :: thesis: verum