set f = primesFinS k;
let n be Nat; :: according to NUMBER13:def 4 :: thesis: ( 1 <= n & n <= len (primesFinS k) implies (primesFinS k) . n >= 1 )
assume that
A1: 1 <= n and
A2: n <= len (primesFinS k) ; :: thesis: (primesFinS k) . n >= 1
reconsider m = n - 1 as Element of NAT by A1, INT_1:3;
A3: len (primesFinS k) = k by Def1;
m + 0 < m + 1 by XREAL_1:8;
then m < k by A2, A3, XXREAL_0:2;
then (primesFinS k) . (m + 1) = primenumber m by Def1;
hence (primesFinS k) . n >= 1 by INT_2:def 4; :: thesis: verum