let n be non zero Nat; :: thesis: support (pfexp n) = PrimeDivisors n
set S = support (pfexp n);
set X = PrimeDivisors n;
thus support (pfexp n) c= PrimeDivisors n :: according to XBOOLE_0:def 10 :: thesis: PrimeDivisors n c= support (pfexp n)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (pfexp n) or x in PrimeDivisors n )
assume A1: x in support (pfexp n) ; :: thesis: x in PrimeDivisors n
then reconsider x = x as Prime by NAT_3:34;
x divides n by A1, NAT_3:36;
hence x in PrimeDivisors n ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in PrimeDivisors n or x in support (pfexp n) )
assume x in PrimeDivisors n ; :: thesis: x in support (pfexp n)
then ex p being Prime st
( x = p & p divides n ) ;
then (pfexp n) . x <> 0 by NAT_3:38;
hence x in support (pfexp n) by PRE_POLY:def 7; :: thesis: verum