theorem Th42: :: NUMBER15:42

for s being Nat holds len (PrimeNumbersFS s) = s