theorem Th28: :: NAT_5:28

for I being set
for f, g being Function of I,NAT
for J, K being finite Subset of I holds Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K))