let I be set ; :: thesis: for x1, A, x2, B being ManySortedSet of 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 ; :: 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 & A is non-empty ) and
A2: [|x1,A|] = [|x2,B|] ; :: thesis: ( x1 = x2 & A = B )
thus x1 = x2 :: thesis: A = B

proof

now

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

end;

hence x1 = x2 by PBOOLE:3; :: thesis: verum

end;

now

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

end;

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