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

now

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

end;

hence x1 = x2 by PBOOLE:3; :: thesis: A = B

now

let i be set ; :: thesis: ( i in I implies A . i = B . i )
assume A7: i in I ; :: thesis: A . i = B . i
then A8: not x1 . i is empty by A1, PBOOLE:def 16;
A9: not A . i is empty by A2, A7, PBOOLE:def 16;
[:(x1 . i),(A . i):] = [|x1,A|] . i by A7, PBOOLE:def 21
.= [:(x2 . i),(B . i):] by A3, A7, PBOOLE:def 21 ;
hence A . i = B . i by A8, A9, ZFMISC_1:134; :: thesis: verum

end;

hence A = B by PBOOLE:3; :: thesis: verum