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