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 . b1 = it2 . b1 )
assume i in SetPrimes ; :: thesis: it1 . b1 = it2 . b1
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 . b1 = it2 . b1
hence it1 . i = p by A12
.= it2 . i by A14, A15 ;
:: thesis: verum
end;
suppose A16: not p in support (pfexp n) ; :: thesis: it1 . b1 = it2 . b1
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