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