let p be Prime; :: thesis: for k being Nat st k >= 1 holds
card (PrimeDivisors (p |^ k)) = 1
let k be Nat; :: thesis: ( k >= 1 implies card (PrimeDivisors (p |^ k)) = 1 )
assume k >= 1 ; :: thesis: card (PrimeDivisors (p |^ k)) = 1
then PrimeDivisors (p |^ k) = {p} by NUMBER12:50;
hence card (PrimeDivisors (p |^ k)) = 1 by CARD_2:42; :: thesis: verum