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 (<*G*> ^ f) = G + (Sum f)
let f be FinSequence of PFuncs (D,REAL); :: thesis: for G being Element of PFuncs (D,REAL) holds Sum (<*G*> ^ f) = G + (Sum f)
let G be Element of PFuncs (D,REAL); :: thesis: Sum (<*G*> ^ f) = G + (Sum f)
thus Sum (<*G*> ^ f) = (Sum <*G*>) + (Sum f) by Th21
.= G + (Sum f) by FINSOP_1:11 ; :: thesis: verum