for m being INT -valued FinSequence
for i being Nat st i in dom m holds
ex z being Integer st z * (m . i) = Product m