theorem Th44: :: NUMBER15:44

for n being non zero Nat
for s being Nat st n <= s holds
(PrimeNumbersFS s) . n = primenumber (n - 1)