let n be Nat; :: thesis: ( n is having_exactly_one_prime_divisor implies ex k being non zero Nat st n = (the_only_divisor_of n) |^ k )
assume A1: n is having_exactly_one_prime_divisor ; :: thesis: ex k being non zero Nat st n = (the_only_divisor_of n) |^ k
then consider p being Prime such that
A2: p divides n and
A3: for r being Prime st r <> p holds
not r divides n ;
A4: the_only_divisor_of n = p by A1, A2, Def7;

now :: thesis: not for k being Nat holds n <> p |^ k

assume for k being Nat holds n <> p |^ k ; :: thesis: contradiction
then ex s being Element of NAT st
( s is prime & s divides n & s <> p ) by GROUPP_1:1;
hence contradiction by A3; :: thesis: verum

end;

then consider k being Nat such that
A5: n = (the_only_divisor_of n) |^ k by A4;
reconsider k = k as non zero Nat by A1, A5;
take k ; :: thesis: n = (the_only_divisor_of n) |^ k
thus n = (the_only_divisor_of n) |^ k by A5; :: thesis: verum