let k be Nat; :: thesis: for p being Prime st primeindex p < k holds
1 + (primeindex p) in dom (primesFinS k)
let p be Prime; :: thesis: ( primeindex p < k implies 1 + (primeindex p) in dom (primesFinS k) )
set i = primeindex p;
assume primeindex p < k ; :: thesis: 1 + (primeindex p) in dom (primesFinS k)
then A1: (primeindex p) + 1 <= k by NAT_1:13;
A2: len (primesFinS k) = k by Def1;
0 + 1 <= (primeindex p) + 1 by XREAL_1:6;
hence 1 + (primeindex p) in dom (primesFinS k) by A1, A2, FINSEQ_3:25; :: thesis: verum