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 associative by Th17;
hence Sum (f1 ^ f2) = (addpfunc D) . (Sum f1),(Sum f2) by Th20, FINSOP_1:6
.= (Sum f1) + (Sum f2) by Def4 ;
:: thesis: verum