let D be non empty set ; :: thesis: for f1, f2 being FinSequence of PFuncs D,REAL holds Sum (f1 ^ f2) = (Sum f1) + (Sum f2)
let f1, f2 be FinSequence of PFuncs D,REAL ; :: thesis: Sum (f1 ^ f2) = (Sum f1) + (Sum f2)
set o = addpfunc D;
( addpfunc D is commutative & addpfunc D is associative & addpfunc D is having_a_unity ) by Th16, Th17, Th20;
hence Sum (f1 ^ f2) = (addpfunc D) . (Sum f1),(Sum f2) by FINSOP_1:6
.= (Sum f1) + (Sum f2) by Def4 ;
:: thesis: verum