let n be non zero Nat; :: thesis: for p being Prime st support (pfexp n) = {p} holds
n = p |^ ((pfexp n) . p)
let p be Prime; :: thesis: ( support (pfexp n) = {p} implies n = p |^ ((pfexp n) . p) )
assume A1: support (pfexp n) = {p} ; :: thesis: n = p |^ ((pfexp n) . p)
set b = ppf n;
consider f being FinSequence of COMPLEX such that
A2: Product (ppf n) = Product f and
A3: f = (ppf n) * (canFS (support (ppf n))) by NAT_3:def 5;
A4: support (pfexp n) = support (ppf n) by NAT_3:def 9;
then A5: ( p in support (ppf n) & support (ppf n) c= dom (ppf n) ) by A1, PRE_POLY:37, TARSKI:def 1;
f = (ppf n) * <*p*> by A3, A1, A4, FINSEQ_1:94
.= <*((ppf n) . p)*> by A5, FINSEQ_2:34 ;
then Product (ppf n) = p |^ (p |-count n) by A2, A5, A4, NAT_3:def 9;
then n = p |^ (p |-count n) by NAT_3:61;
hence n = p |^ ((pfexp n) . p) by NAT_3:def 8; :: thesis: verum