theorem Th97: :: RVSUM_1:97

for F1, F2 being complex-valued FinSequence holds Product (F1 ^ F2) = (Product F1) * (Product F2)