theorem Th24: :: NAT_5:24

for f being sequence of NAT
for F being sequence of REAL
for J being finite Subset of NAT st f = F & ex k being Nat st J c= Seg k holds
Sum (f | J) = Sum (Func_Seq (F,(Sgm J)))