defpred S1[ 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 & S1[x,y1] & S1[x,y2] holds
y1 = y2
A5:
for x being object st x in SetPrimes holds
ex y being object st S1[x,y]
consider f being Function such that
A9:
dom f = SetPrimes
and
A10:
for x being object st x in SetPrimes holds
S1[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)
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
; ( 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
hence
support f = support (pfexp n)
by A12, XBOOLE_0:def 10; for p being Nat st p in support (pfexp n) holds
f . p = p |^ (2 * ((p |-count n) div 2))
let p be Nat; ( p in support (pfexp n) implies f . p = p |^ (2 * ((p |-count n) div 2)) )
assume A15:
p in support (pfexp n)
; 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; verum