theorem Th32: :: NUMBER08:32

for f1, f2 being integer-valued FinSequence st len f1 = len f2 & ( for n being Nat st 1 <= n & n <= len f1 holds
f1 . n divides f2 . n ) holds
Product f1 divides Product f2