let it1, it2 be ManySortedSet of X; :: thesis: ( support it1 = support b & ( for i being object holds it1 . i = (b . i) |^ n ) & support it2 = support b & ( for i being object holds it2 . i = (b . i) |^ n ) implies it1 = it2 )
assume that
support it1 = support b and
A11: for i being object holds it1 . i = (b . i) |^ n and
support it2 = support b and
A12: for i being object holds it2 . i = (b . i) |^ n ; :: thesis: it1 = it2
now :: thesis: for x being object st x in X holds
it1 . x = it2 . x
let x be object ; :: thesis: ( x in X implies it1 . x = it2 . x )
assume x in X ; :: thesis: it1 . x = it2 . x
thus it1 . x = (b . x) |^ n by A11
.= it2 . x by A12 ; :: thesis: verum
end;
hence it1 = it2 ; :: thesis: verum