theorem :: RVSUM_2:42

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