let I be set ; :: thesis: for X, Y being ManySortedSet of I st [|X,X|] = [|Y,Y|] holds
X = Y
let X, Y be ManySortedSet of I; :: thesis: ( [|X,X|] = [|Y,Y|] implies X = Y )
assume A1: [|X,X|] = [|Y,Y|] ; :: thesis: X = Y

now :: thesis: for i being object st i in I holds
X . i = Y . i

let i be object ; :: thesis: ( i in I implies X . i = Y . i )
assume A2: i in I ; :: thesis: X . i = Y . i
then [:(X . i),(X . i):] = [|X,X|] . i by PBOOLE:def 16
.= [:(Y . i),(Y . i):] by A1, A2, PBOOLE:def 16 ;
hence X . i = Y . i by ZFMISC_1:92; :: thesis: verum

end;

hence X = Y ; :: thesis: verum