theorem Th9: :: INT_6:9

for m being integer-valued FinSequence
for i being Nat holds (Product m) / (m . i) is Integer