let I be set ; :: thesis: for X, Y being ManySortedSet of st X is non-empty & Y is non-empty & [|X,Y|] = [|Y,X|] holds
X = Y
let X, Y be ManySortedSet of ; :: thesis: ( X is non-empty & Y is non-empty & [|X,Y|] = [|Y,X|] implies X = Y )
assume that
A1: ( X is non-empty & Y is non-empty ) and
A2: [|X,Y|] = [|Y,X|] ; :: thesis: X = Y

now

let i be set ; :: thesis: ( i in I implies X . i = Y . i )
assume A3: i in I ; :: thesis: X . i = Y . i
then A4: ( not X . i is empty & not Y . i is empty ) by A1, PBOOLE:def 16;
[:(X . i),(Y . i):] = [|X,Y|] . i by A3, PBOOLE:def 21
.= [:(Y . i),(X . i):] by A2, A3, PBOOLE:def 21 ;
hence X . i = Y . i by A4, ZFMISC_1:114; :: thesis: verum

end;

hence X = Y by PBOOLE:3; :: thesis: verum