let a be natural number ; :: thesis: for p being Prime st a <> 0 holds
support (pfexp (p |^ a)) = {p}
let p be Prime; :: thesis: ( a <> 0 implies support (pfexp (p |^ a)) = {p} )
set f = pfexp (p |^ a);
assume A1: a <> 0 ; :: thesis: support (pfexp (p |^ a)) = {p}
thus support (pfexp (p |^ a)) c= {p} :: according to XBOOLE_0:def 10 :: thesis: {p} c= support (pfexp (p |^ a))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in support (pfexp (p |^ a)) or x in {p} )
assume A2: x in support (pfexp (p |^ a)) ; :: thesis: x in {p}
then reconsider x = x as Prime by Th34;
A3: (pfexp (p |^ a)) . x <> 0 by A2, POLYNOM1:def 7;
A4: x <> 1 by INT_2:def 5;
(pfexp (p |^ a)) . x = x |-count (p |^ a) by Def8;
then x divides p |^ a by A3, A4, Th27;
then x = p by Th6;
hence x in {p} by TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {p} or x in support (pfexp (p |^ a)) )
assume x in {p} ; :: thesis: x in support (pfexp (p |^ a))
then A5: x = p by TARSKI:def 1;
p divides p |^ a by A1, Th3;
then (pfexp (p |^ a)) . p <> 0 by Th38;
hence x in support (pfexp (p |^ a)) by A5, POLYNOM1:def 7; :: thesis: verum