let f, g be ManySortedSet of SetPrimes ; :: thesis: ( ( for p being Prime holds f . p = p |-count n ) & ( for p being Prime holds g . p = p |-count n ) implies f = g )
assume that
A3: for i being Prime holds f . i = i |-count n and
A4: for i being Prime holds g . i = i |-count n ; :: thesis: f = g
now :: thesis: for i being object st i in SetPrimes holds
f . i = g . i
let i be object ; :: thesis: ( i in SetPrimes implies f . i = g . i )
assume i in SetPrimes ; :: thesis: f . i = g . i
then reconsider a = i as prime Element of NAT by NEWTON:def 6;
thus f . i = a |-count n by A3
.= g . i by A4 ; :: thesis: verum
end;
hence f = g ; :: thesis: verum