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

now

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

end;

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