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