defpred S₁[ object , object ] means for p being Prime st $1 = p holds
( ( p in support (pfexp n) implies $2 = p |^ (p |-count n) ) & ( not p in support (pfexp n) implies $2 = 0 ) );
A1: for x being object st x in SetPrimes holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in SetPrimes implies ex y being object st S₁[x,y] )
assume x in SetPrimes ; :: thesis: ex y being object st S₁[x,y]
then reconsider i = x as prime Element of NAT by NEWTON:def 6;

per cases ( i in support (pfexp n) or not i in support (pfexp n) ) ;

suppose A2: i in support (pfexp n) ; :: thesis: ex y being object st S₁[x,y]

take i |^ (i |-count n) ; :: thesis: S₁[x,i |^ (i |-count n)]
let p be Prime; :: thesis: ( x = p implies ( ( p in support (pfexp n) implies i |^ (i |-count n) = p |^ (p |-count n) ) & ( not p in support (pfexp n) implies i |^ (i |-count n) = 0 ) ) )
assume p = x ; :: thesis: ( ( p in support (pfexp n) implies i |^ (i |-count n) = p |^ (p |-count n) ) & ( not p in support (pfexp n) implies i |^ (i |-count n) = 0 ) )
hence ( ( p in support (pfexp n) implies i |^ (i |-count n) = p |^ (p |-count n) ) & ( not p in support (pfexp n) implies i |^ (i |-count n) = 0 ) ) by A2; :: thesis: verum

end;

suppose A3: not i in support (pfexp n) ; :: thesis: ex y being object st S₁[x,y]

take 0 ; :: thesis: S₁[x, 0 ]
let p be Prime; :: thesis: ( x = p implies ( ( p in support (pfexp n) implies 0 = p |^ (p |-count n) ) & ( not p in support (pfexp n) implies 0 = 0 ) ) )
assume p = x ; :: thesis: ( ( p in support (pfexp n) implies 0 = p |^ (p |-count n) ) & ( not p in support (pfexp n) implies 0 = 0 ) )
hence ( ( p in support (pfexp n) implies 0 = p |^ (p |-count n) ) & ( not p in support (pfexp n) implies 0 = 0 ) ) by A3; :: thesis: verum

end;

end;

end;

consider f being Function such that
A4: dom f = SetPrimes and
A5: for x being object st x in SetPrimes holds
S₁[x,f . x] from CLASSES1:sch 1(A1);
A6: support f c= SetPrimes by A4, PRE_POLY:37;

A7: now :: thesis: for x being object holds
( ( x in support f implies x in support (pfexp n) ) & ( x in support (pfexp n) implies x in support f ) )

let x be object ; :: thesis: ( ( x in support f implies x in support (pfexp n) ) & ( x in support (pfexp n) implies x in support f ) )

hereby :: thesis: ( x in support (pfexp n) implies x in support f )

assume A8: x in support f ; :: thesis: x in support (pfexp n)
then x in SetPrimes by A6;
then reconsider i = x as prime Element of NAT by NEWTON:def 6;
assume not x in support (pfexp n) ; :: thesis: contradiction
then f . i = 0 by A5, A6, A8;
hence contradiction by A8, PRE_POLY:def 7; :: thesis: verum

end;

assume A9: x in support (pfexp n) ; :: thesis: x in support f
then x in SetPrimes ;
then reconsider i = x as prime Element of NAT by NEWTON:def 6;
f . i = i |^ (i |-count n) by A5, A9;
hence x in support f by PRE_POLY:def 7; :: thesis: verum

end;

reconsider f = f as ManySortedSet of SetPrimes by A4, PARTFUN1:def 2, RELAT_1:def 18;
take f ; :: thesis: ( support f = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
f . p = p |^ (p |-count n) ) )
thus support f = support (pfexp n) by A7, TARSKI:2; :: thesis: for p being Nat st p in support (pfexp n) holds
f . p = p |^ (p |-count n)
let p be Nat; :: thesis: ( p in support (pfexp n) implies f . p = p |^ (p |-count n) )
assume A10: p in support (pfexp n) ; :: thesis: f . p = p |^ (p |-count n)
then p is Prime by Th34;
hence f . p = p |^ (p |-count n) by A5, A10; :: thesis: verum