theorem Th9: :: JORDAN2B:9

for i being Element of NAT holds Sum (0* i) = 0