for rr being Real holds Product (0 |-> rr) = 1 by RVSUM_1:94;