theorem Th24: :: NAT_5:24

for f being sequence of NAT
for F being sequence of REAL
for J being included_in_Seg Subset of NAT st f = F holds
Sum (f | J) = Sum (Func_Seq (F,(Sgm J)))