theorem :: NAT_3:8

for p being Prime
for f being FinSequence of SetPrimes st p divides Product f holds
p in rng f