for a being Nat
for f being FinSequence of NAT st a in rng f holds
a divides Product f