theorem Th27: :: NAT_5:27

for I being set
for f being Function of I,NAT
for J being finite Subset of I
for j being object st J = {j} holds
Sum (f | J) = f . j