theorem :: INT_6:12

for m being INT -valued FinSequence
for i, j being Nat st i in dom m & i <> j holds
ex z being Integer st z * (m . i) = (Product m) / (m . j) by Lm6;