n >= 1 by NAT_1:14;

per cases then ( n = 1 or n > 1 ) by XXREAL_0:1;

suppose A1: n = 1 ; :: thesis: ex b₁ being Function st
( dom b₁ = support (ppf n) & ( for p being Nat st p in dom b₁ holds
ex c being non zero Nat st
( c = p |-count n & b₁ . p = p |^ (c - 1) ) ) )

take {} ; :: thesis: ( dom {} = support (ppf n) & ( for p being Nat st p in dom {} holds
ex c being non zero Nat st
( c = p |-count n & {} . p = p |^ (c - 1) ) ) )
support (ppf 1) = support (pfexp 1) by NAT_3:def 9;
hence ( dom {} = support (ppf n) & ( for p being Nat st p in dom {} holds
ex c being non zero Nat st
( c = p |-count n & {} . p = p |^ (c - 1) ) ) ) by A1; :: thesis: verum

end;

suppose n > 1 ; :: thesis: ex b₁ being Function st
( dom b₁ = support (ppf n) & ( for p being Nat st p in dom b₁ holds
ex c being non zero Nat st
( c = p |-count n & b₁ . p = p |^ (c - 1) ) ) )

then reconsider A = support (ppf n) as non empty natural-membered set by NAT_3:57;
A2: A = support (pfexp n) by NAT_3:def 9;
defpred S₁[ object , object ] means ex a being Nat st
( a = $1 & ex c being non zero Nat st
( c = a |-count n & $2 = a |^ (c - 1) ) );
A3: for e being object st e in A holds
ex u being object st S₁[e,u]

proof

let e be object ; :: thesis: ( e in A implies ex u being object st S₁[e,u] )
assume A4: e in A ; :: thesis: ex u being object st S₁[e,u]
then reconsider e = e as Prime by A2, NAT_3:34;
A5: e > 1 by INT_2:def 4;
set c = e |-count n;

now :: thesis: not e |-count n = 0

assume e |-count n = 0 ; :: thesis: contradiction
then A6: not e divides n by A5, NAT_3:27;
e in support (pfexp n) by A4, NAT_3:def 9;
hence contradiction by A6, NAT_3:36; :: thesis: verum

end;

then reconsider c = e |-count n as non zero Nat ;
take e |^ (c - 1) ; :: thesis: S₁[e,e |^ (c - 1)]
thus S₁[e,e |^ (c - 1)] ; :: thesis: verum

end;

consider f being Function such that
A7: dom f = A and
A8: for e being object st e in A holds
S₁[e,f . e] from CLASSES1:sch 1(A3);
take f ; :: thesis: ( dom f = support (ppf n) & ( for p being Nat st p in dom f holds
ex c being non zero Nat st
( c = p |-count n & f . p = p |^ (c - 1) ) ) )
thus dom f = support (ppf n) by A7; :: thesis: for p being Nat st p in dom f holds
ex c being non zero Nat st
( c = p |-count n & f . p = p |^ (c - 1) )
let p be Nat; :: thesis: ( p in dom f implies ex c being non zero Nat st
( c = p |-count n & f . p = p |^ (c - 1) ) )
assume A9: p in dom f ; :: thesis: ex c being non zero Nat st
( c = p |-count n & f . p = p |^ (c - 1) )
A = support (pfexp n) by NAT_3:def 9;
then reconsider p = p as Prime by A7, A9, NAT_3:34;
A10: p > 1 by INT_2:def 4;
set c = p |-count n;

now :: thesis: not p |-count n = 0

assume p |-count n = 0 ; :: thesis: contradiction
then A11: not p divides n by A10, NAT_3:27;
p in support (pfexp n) by A7, A9, NAT_3:def 9;
hence contradiction by A11, NAT_3:36; :: thesis: verum

end;

then reconsider c = p |-count n as non zero Nat ;
take c ; :: thesis: ( c = p |-count n & f . p = p |^ (c - 1) )
S₁[p,f . p] by A7, A8, A9;
hence ( c = p |-count n & f . p = p |^ (c - 1) ) ; :: thesis: verum

end;

end;