theorem Th26: :: NAT_5:26

for I being set
for f being Function of I,NAT
for J, K being finite Subset of I st J misses K holds
Sum (f | (J \/ K)) = (Sum (f | J)) + (Sum (f | K))