let it1, it2 be ManySortedSet of ; :: thesis: ( support it1 = support (pfexp n) & ( for p being natural number st p in support (pfexp n) holds
it1 . p = p ) & support it2 = support (pfexp n) & ( for p being natural number st p in support (pfexp n) holds
it2 . p = p ) implies it1 = it2 )
assume that
A16: support it1 = support (pfexp n) and
A17: for p being natural number st p in support (pfexp n) holds
it1 . p = p and
A18: support it2 = support (pfexp n) and
A19: for p being natural number st p in support (pfexp n) holds
it2 . p = p ; :: thesis: it1 = it2

now

let i be set ; :: thesis: ( i in SetPrimes implies it1 . b₁ = it2 . b₁ )
assume A20: i in SetPrimes ; :: thesis: it1 . b₁ = it2 . b₁
reconsider p = i as prime Element of NAT 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: it1 . b₁ = it2 . b₁

hence it1 . i = p by A17
.= it2 . i by A19, A21 ;
:: thesis: verum

end;

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

hence it1 . i = 0 by A16, POLYNOM1:def 7
.= it2 . i by A18, A22, POLYNOM1:def 7 ;
:: thesis: verum

end;

end;

end;

hence it1 = it2 by PBOOLE:3; :: thesis: verum