theorem :: RVSUM_1:76

for r being Real
for F being real-valued FinSequence holds Sum (<*r*> ^ F) = r + (Sum F)