set h = primesFinS k;
let i be Nat; :: according to EUCLID_7:def 1 :: thesis: ( not 1 <= i or len (primesFinS k) <= i or not (primesFinS k) . K247(i,1) <= (primesFinS k) . i )
assume that
A1: 1 <= i and
A2: i < len (primesFinS k) ; :: thesis: not (primesFinS k) . K247(i,1) <= (primesFinS k) . i
reconsider j = i - 1 as Element of NAT by A1, INT_1:3;
A3: j + 0 < j + 1 by XREAL_1:8;
A4: len (primesFinS k) = k by Def1;
then j < k by A2, A3, XXREAL_0:2;
then A5: (primesFinS k) . (j + 1) = primenumber j by Def1;
(primesFinS k) . (i + 1) = primenumber i by A2, A4, Def1;
hence (primesFinS k) . i < (primesFinS k) . (i + 1) by A3, A5, MOEBIUS2:21; :: thesis: verum