theorem FAF: :: RVSUM_4:10

for f, g being complex-valued FinSequence holds Product (f ^ g) = (Product f) * (Product g)