theorem Th94: :: RVSUM_1:94

Product (<*> REAL) = 1 by Lm3;