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;
( addpfunc D is commutative & addpfunc D is associative & addpfunc D is having_a_unity ) by Th16, Th17, Th20;
hence Sum (f ^ <*G*>) = (addpfunc D) . ((addpfunc D) $$ f),G by FINSOP_1:5
.= (Sum f) + G by Def4 ;
:: thesis: verum