for n, i being Element of NAT
for r being Real st i in Seg n holds
Sum ((0* n) +* (i,r)) = r