theorem Th48: :: RVSUM_2:48

for i being Nat
for R1, R2 being b₁ -element complex-valued FinSequence holds Product (mlt (R1,R2)) = (Product R1) * (Product R2)