set f = primesFinS k;
let n be Nat; :: according to RVSUM_3:def 1 :: thesis: ( not n in dom (primesFinS k) or not (primesFinS k) . n <= 0 )
assume A1: n in dom (primesFinS k) ; :: thesis: not (primesFinS k) . n <= 0
then 1 <= n by FINSEQ_3:25;
then reconsider m = n - 1 as Element of NAT by INT_1:3;
A2: n <= len (primesFinS k) by A1, FINSEQ_3:25;
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 > 0 ; :: thesis: verum