theorem Th8: :: INTEGR23:6

for p being FinSequence of REAL
for i being Nat
for r being Real st i in dom p & p . i = r & ( for k being Nat st k in dom p & k <> i holds
p . k = 0 ) holds
Sum p = r