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

proof

let x, y1, y2 be object ; :: thesis: ( x in SetPrimes & S₁[x,y1] & S₁[x,y2] implies y1 = y2 )
assume that
A2: x in SetPrimes and
A3: S₁[x,y1] and
A4: S₁[x,y2] ; :: thesis: y1 = y2
reconsider p = x as Prime by A2, NEWTON:def 6;
y1 = y2

proof

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

suppose Z1: p in support (pfexp n) ; :: thesis: y1 = y2

hence y1 = p |^ (2 * ((p |-count n) div 2)) by A3
.= y2 by Z1, A4 ;
:: thesis: verum

end;

suppose Z1: not p in support (pfexp n) ; :: thesis: y1 = y2

hence y1 = 0 by A3
.= y2 by A4, Z1 ;
:: thesis: verum

end;

end;

end;

hence y1 = y2 ; :: thesis: verum

end;

A5: 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 A6: x in SetPrimes ; :: thesis: ex y being object st S₁[x,y]
reconsider i = x as prime Element of NAT by A6, NEWTON:def 6;

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

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

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

end;

suppose A8: 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 |^ (2 * ((p |-count n) div 2)) ) & ( not p in support (pfexp n) implies 0 = 0 ) ) )
assume p = x ; :: thesis: ( ( p in support (pfexp n) implies 0 = p |^ (2 * ((p |-count n) div 2)) ) & ( not p in support (pfexp n) implies 0 = 0 ) )
hence ( ( p in support (pfexp n) implies 0 = p |^ (2 * ((p |-count n) div 2)) ) & ( not p in support (pfexp n) implies 0 = 0 ) ) by A8; :: thesis: verum

end;

end;

end;

consider f being Function such that
A9: dom f = SetPrimes and
A10: for x being object st x in SetPrimes holds
S₁[x,f . x] from FUNCT_1:sch 2(A1, A5);
A11: support f c= SetPrimes by A9, PRE_POLY:37;
A12: support f c= support (pfexp n)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support f or x in support (pfexp n) )
assume A13: x in support f ; :: thesis: x in support (pfexp n)
then reconsider i = x as Prime by A11, NEWTON:def 6;
assume not x in support (pfexp n) ; :: thesis: contradiction
then f . i = 0 by A10, A11, A13;
hence contradiction by A13, PRE_POLY:def 7; :: thesis: verum

end;

reconsider f = f as SetPrimes -defined Function by A9, RELAT_1:def 18;
reconsider f = f as ManySortedSet of SetPrimes by A9, PARTFUN1:def 2;
take f ; :: thesis: ( support f = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
f . p = p |^ (2 * ((p |-count n) div 2)) ) )
support (pfexp n) c= support f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (pfexp n) or x in support f )
assume J0: x in support (pfexp n) ; :: thesis: x in support f
then reconsider p = x as Prime by NAT_3:34;
f . x = p |^ (2 * ((p |-count n) div 2)) by A10, J0;
hence x in support f by PRE_POLY:def 7; :: thesis: verum

end;

hence support f = support (pfexp n) by A12, XBOOLE_0:def 10; :: thesis: for p being Nat st p in support (pfexp n) holds
f . p = p |^ (2 * ((p |-count n) div 2))
let p be Nat; :: thesis: ( p in support (pfexp n) implies f . p = p |^ (2 * ((p |-count n) div 2)) )
assume A15: p in support (pfexp n) ; :: thesis: f . p = p |^ (2 * ((p |-count n) div 2))
then p is Prime by NAT_3:34;
hence f . p = p |^ (2 * ((p |-count n) div 2)) by A15, A10; :: thesis: verum