let f1, f2 be ManySortedSet of SetPrimes ; :: thesis: ( support f1 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
f1 . p = p |^ ((p |-count n) div 2) ) & support f2 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
f2 . p = p |^ ((p |-count n) div 2) ) implies f1 = f2 )
assume that
A16: support f1 = support (pfexp n) and
A17: for p being Nat st p in support (pfexp n) holds
f1 . p = p |^ ((p |-count n) div 2) and
A18: support f2 = support (pfexp n) and
A19: for p being Nat st p in support (pfexp n) holds
f2 . p = p |^ ((p |-count n) div 2) ; :: thesis: f1 = f2

now :: thesis: for i being object st i in SetPrimes holds
f1 . i = f2 . i

let i be object ; :: thesis: ( i in SetPrimes implies f1 . b₁ = f2 . b₁ )
assume A20: i in SetPrimes ; :: thesis: f1 . b₁ = f2 . b₁
reconsider p = i as Prime by A20, NEWTON:def 6;

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

suppose A21: p in support (pfexp n) ; :: thesis: f1 . b₁ = f2 . b₁

hence f1 . i = p |^ ((p |-count n) div 2) by A17
.= f2 . i by A19, A21 ;
:: thesis: verum

end;

suppose A22: not p in support (pfexp n) ; :: thesis: f1 . b₁ = f2 . b₁

hence f1 . i = 0 by A16, PRE_POLY:def 7
.= f2 . i by A18, A22, PRE_POLY:def 7 ;
:: thesis: verum

end;

end;

end;

hence f1 = f2 by PBOOLE:3; :: thesis: verum