theorem Th32: :: NUMBER16:32
for n, m being Nat st ( for k being Nat st k < m holds
primenumber k divides n ) holds
Product (primesFinS m) divides n