theorem Th78: :: NUMBER08:78

for n being Nat st n is having_exactly_one_prime_divisor holds
ex k being non zero Nat st n = (the_only_divisor_of n) |^ k