let it1, it2 be ManySortedSet of X; :: thesis: ( ( for x being set holds it1 . x = (b1 . x) -' (b2 . x) ) & ( for x being set holds it2 . x = (b1 . x) -' (b2 . x) ) implies it1 = it2 )
assume that
A5: for x being set holds it1 . x = (b1 . x) -' (b2 . x) and
A6: for x being set holds it2 . x = (b1 . x) -' (b2 . x) ; :: thesis: it1 = it2

now

let x be set ; :: thesis: ( x in X implies it1 . x = it2 . x )
assume x in X ; :: thesis: it1 . x = it2 . x
thus it1 . x = (b1 . x) -' (b2 . x) by A5
.= it2 . x by A6 ; :: thesis: verum

end;

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