set p = PFactors n;
for x being Prime st x in support (PFactors n) holds
ex n being Nat st
( 0 < n & (PFactors n) . x = x |^ n )

proof

let x be Prime; :: thesis: ( x in support (PFactors n) implies ex n being Nat st
( 0 < n & (PFactors n) . x = x |^ n ) )
assume x in support (PFactors n) ; :: thesis: ex n being Nat st
( 0 < n & (PFactors n) . x = x |^ n )
then a1: x in support (pfexp n) by MOEBIUS1:def 6;
x = x |^ 1 ;
hence ex n being Nat st
( 0 < n & (PFactors n) . x = x |^ n ) by a1, MOEBIUS1:def 6; :: thesis: verum

end;

hence PFactors n is prime-factorization-like by INT_7:def 1; :: thesis: verum