for p being Prime
for f being FinSequence of NAT st f is positive-yielding & p divides Product f holds
ex i being Nat st
( i in dom f & p divides f . i )