theorem :: NUMBER18:20

for s being Nat ex f being increasing positive-yielding fAP-like FinSequence of NAT st
( len f = s & ( for i being Nat st 1 <= i & i <= len f holds
not f . i is prime ) )