defpred S₁[ Nat] means 2 |^ $1 <= Product (primesFinS $1);
A1: Product (primesFinS 0) = 1 by RVSUM_1:94;
2 |^ 0 = 1 by NEWTON:4;
then A2: S₁[ 0 ] by A1;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
set n1 = n + 1;
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
A5: Product (primesFinS (n + 1)) = (Product (primesFinS n)) * (primenumber n) by Th25;
2 <= primenumber n by MOEBIUS2:8, MOEBIUS2:21;
then 2 * (2 |^ n) <= Product (primesFinS (n + 1)) by A5, A4, XREAL_1:66;
hence S₁[n + 1] by NEWTON:6; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
hence for k being Nat holds 2 |^ k <= Product (primesFinS k) ; :: thesis: verum