let n, s be Nat; :: thesis: ( n < s implies (PrimeNumbersFS s) . (n + 1) = primenumber n )
set h = PrimeNumbersS s;
set q = (PrimeNumbersS s) | s;
assume A1: n < s ; :: thesis: (PrimeNumbersFS s) . (n + 1) = primenumber n
then A2: n in Segm s by NAT_1:44;
n + 1 <= len ((PrimeNumbersS s) | s) by A1, NAT_1:13;
hence (PrimeNumbersFS s) . (n + 1) = ((PrimeNumbersS s) | s) . ((n + 1) - 1) by NAT_1:11, AFINSQ_1:def 9
.= (PrimeNumbersS s) . n by A2, FUNCT_1:49
.= primenumber n by Def3 ;
:: thesis: verum