let i be Element of NAT ; :: thesis: Sum (0* i) = 0
thus Sum (0* i) = i * 0 by RVSUM_1:80
.= 0 ; :: thesis: verum