let i be natural Number ; :: thesis: Sum (i |-> 0) = 0
thus Sum (i |-> 0) = i * 0 by Th80
.= 0 ; :: thesis: verum