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 Th24
.= G + (Sum f) by FINSOP_1:12 ; :: thesis: verum