theorem Th9: :: INT_6:9

for m being INT -valued FinSequence
for i being Nat st i in dom m & m . i <> 0 holds
(Product m) / (m . i) is Integer