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