theorem Th31: :: NUMBER16:31

for n being Nat holds
( rng (prime_exponents (Product (primesFinS n))) c= {0,1} & card (support (prime_exponents (Product (primesFinS n)))) = n )