defpred S₁[ object , object ] means for p being Prime st $1 = p holds
( ( p in support (pfexp n) implies $2 = p ) & ( 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]

let x be object ; :: thesis:
assume x in SetPrimes ; :: thesis:
then reconsider i = x as prime Element of NAT by NEWTON:def 6;

suppose A2: i in support (pfexp n) ; :: thesis:

take i ; :: thesis:
let p be Prime; :: thesis:
assume p = x ; :: thesis:
hence ( ( p in support (pfexp n) implies i = p ) & ( not p in support (pfexp n) implies i = 0 ) ) by A2; :: thesis:

end;

suppose A3: not i in support (pfexp n) ; :: thesis:

take 0 ; :: thesis:
let p be Prime; :: thesis:
assume p = x ; :: thesis:
hence ( ( p in support (pfexp n) implies 0 = p ) & ( not p in support (pfexp n) implies 0 = 0 ) ) by A3; :: thesis:

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:

let x be object ; :: thesis:

hereby :: thesis:

assume A8: x in support f ; :: thesis:
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:
then f . i = 0 by A5, A6, A8;
hence contradiction by A8, PRE_POLY:def 7; :: thesis:

end;

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

end;

reconsider f = f as ManySortedSet of SetPrimes by A4, PARTFUN1:def 2, RELAT_1:def 18;
take f ; :: thesis:
thus support f = support (pfexp n) by A7, TARSKI:2; :: thesis:
let p be Nat; :: thesis:
assume A10: p in support (pfexp n) ; :: thesis:
then p is Prime by NAT_3:34;
hence f . p = p by A5, A10; :: thesis: