theorem :: INT_6:11

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