theorem Th13: :: NUMBER13:13

for k being Nat
for p being Prime st primeindex p < k holds
1 + (primeindex p) in dom (primesFinS k)