let k, s be Nat; :: thesis: ( k < s implies (Product (PrimeNumbersFS s)) / (primenumber k) is Nat )
assume k < s ; :: thesis: (Product (PrimeNumbersFS s)) / (primenumber k) is Nat
then (PrimeNumbersFS s) . (k + 1) = primenumber k by Th43;
hence (Product (PrimeNumbersFS s)) / (primenumber k) is Nat ; :: thesis: verum