let k be Nat; :: thesis: for p being Prime st p < primenumber k holds
p in rng (primesFinS k)
let p be Prime; :: thesis: ( p < primenumber k implies p in rng (primesFinS k) )
set f = primesFinS k;
set i = primeindex p;
assume A1: p < primenumber k ; :: thesis: p in rng (primesFinS k)
then A2: 1 + (primeindex p) in dom (primesFinS k) by Th13, Th12;
(primesFinS k) . (1 + (primeindex p)) = p by A1, Th12, Th14;
hence p in rng (primesFinS k) by A2, FUNCT_1:def 3; :: thesis: verum