let n be odd Nat; :: thesis: ( card (PrimeDivisors n) = 1 implies ex k being Nat ex p being Prime st n = p |^ k )
assume card (PrimeDivisors n) = 1 ; :: thesis: ex k being Nat ex p being Prime st n = p |^ k
then consider x being object such that
A2: PrimeDivisors n = {x} by CARD_2:42;
x in PrimeDivisors n by A2, TARSKI:def 1;
then consider p being Prime such that
A3: ( x = p & p divides n ) ;
set k = p |-count n;
( p |-count n >= 1 & n = p |^ (p |-count n) ) by A2, A3, OnlyOddPrimeX;
hence ex k being Nat ex p being Prime st n = p |^ k ; :: thesis: verum