let it1, it2 be ManySortedSet of SetPrimes ; :: thesis: ( support it1 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
it1 . p = p ) & support it2 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
it2 . p = p ) implies it1 = it2 )
assume that
A11: support it1 = support (pfexp n) and
A12: for p being Nat st p in support (pfexp n) holds
it1 . p = p and
A13: support it2 = support (pfexp n) and
A14: for p being Nat st p in support (pfexp n) holds
it2 . p = p ; :: thesis: it1 = it2

now :: thesis: for i being object st i in SetPrimes holds
it1 . i = it2 . i

let i be object ; :: thesis: ( i in SetPrimes implies it1 . b₁ = it2 . b₁ )
assume i in SetPrimes ; :: thesis: it1 . b₁ = it2 . b₁
then reconsider p = i as prime Element of NAT by NEWTON:def 6;

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

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

hence it1 . i = p by A12
.= it2 . i by A14, A15 ;
:: thesis: verum

end;

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

hence it1 . i = 0 by A11, PRE_POLY:def 7
.= it2 . i by A13, A16, PRE_POLY:def 7 ;
:: thesis: verum

end;

end;

end;

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