let k be Nat; :: thesis: for p being Prime st p, Product (primesFinS k) are_coprime holds
primenumber k <= p
let p be Prime; :: thesis: ( p, Product (primesFinS k) are_coprime implies primenumber k <= p )
set f = primesFinS k;
set P = Product (primesFinS k);
assume A1: p, Product (primesFinS k) are_coprime ; :: thesis: primenumber k <= p
assume primenumber k > p ; :: thesis: contradiction
then p in rng (primesFinS k) by Th15;
then p divides Product (primesFinS k) by NAT_3:7;
hence contradiction by A1, PYTHTRIP:def 2; :: thesis: verum