let s be Nat; :: thesis: len (PrimeNumbersFS s) = s
len (PrimeNumbersFS s) = len ((PrimeNumbersS s) | s) by AFINSQ_1:def 9;
hence len (PrimeNumbersFS s) = s ; :: thesis: verum