let k be Nat; :: thesis: for p being Prime st primeindex p < k holds
(primesFinS k) . (1 + (primeindex p)) = p
let p be Prime; :: thesis: ( primeindex p < k implies (primesFinS k) . (1 + (primeindex p)) = p )
set i = primeindex p;
assume primeindex p < k ; :: thesis: (primesFinS k) . (1 + (primeindex p)) = p
then (primesFinS k) . ((primeindex p) + 1) = primenumber (primeindex p) by Def1;
hence (primesFinS k) . (1 + (primeindex p)) = p by NUMBER10:def 4; :: thesis: verum