let n be non zero Nat; :: thesis: for s being Nat st n <= s holds
(PrimeNumbersFS s) . n = primenumber (n - 1)
let s be Nat; :: thesis: ( n <= s implies (PrimeNumbersFS s) . n = primenumber (n - 1) )
reconsider n1 = n - 1 as Element of NAT by INT_1:3;
assume A1: n <= s ; :: thesis: (PrimeNumbersFS s) . n = primenumber (n - 1)
n1 < n - 0 by XREAL_1:8;
then n1 < s by A1, XXREAL_0:2;
then (PrimeNumbersFS s) . (n1 + 1) = primenumber n1 by Th43;
hence (PrimeNumbersFS s) . n = primenumber (n - 1) ; :: thesis: verum