theorem PRN: :: NEWTON04:63

for n being Nat
for f, g being b₁ -element complex-valued FinSequence holds Product (f (#) g) = (Product f) * (Product g) by RVSUM_2:48;