theorem Th25: :: NUMBER16:25

for n being Nat holds Product (primesFinS (n + 1)) = (Product (primesFinS n)) * (primenumber n)