let a be Nat; :: 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 a <> 0 ; :: thesis: support (pfexp (p |^ a)) = {p}
then p divides p |^ a by Th3;
then A1: (pfexp (p |^ a)) . p <> 0 by Th38;
thus support (pfexp (p |^ a)) c= {p} :: according to XBOOLE_0:def 10 :: thesis: {p} c= support (pfexp (p |^ a))
proof
let x be object ; :: 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: ( x <> 1 & (pfexp (p |^ a)) . x = x |-count (p |^ a) ) by Def8, INT_2:def 4;
(pfexp (p |^ a)) . x <> 0 by A2, PRE_POLY:def 7;
then x divides p |^ a by A3, Th27;
then x = p by Th6;
hence x in {p} by TARSKI:def 1; :: thesis: verum
end;
let x be object ; :: 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 x = p by TARSKI:def 1;
hence x in support (pfexp (p |^ a)) by A1, PRE_POLY:def 7; :: thesis: verum