theorem Th21: :: EUCLID_7:22

for n being Nat
for k being Element of NAT holds Sum (k |-> (0* n)) = 0* n