theorem :: RVSUM_1:102

for i being natural Number holds Product (i |-> 1) = 1