theorem Th21: :: EUCLID_7:22

for n, k being Nat holds Sum (k |-> (0* n)) = 0* n