let I, J be set ; :: thesis: for A being ManySortedSet of I

for B being ManySortedSet of J st A cc= B & B cc= A holds

A = B

let A be ManySortedSet of I; :: thesis: for B being ManySortedSet of J st A cc= B & B cc= A holds

A = B

let B be ManySortedSet of J; :: thesis: ( A cc= B & B cc= A implies A = B )

assume that

A1: A cc= B and

A2: B cc= A ; :: thesis: A = B

A3: I c= J by A1;

J c= I by A2;

then I = J by A3, XBOOLE_0:def 10;

then reconsider B9 = B as ManySortedSet of I ;

for B being ManySortedSet of J st A cc= B & B cc= A holds

A = B

let A be ManySortedSet of I; :: thesis: for B being ManySortedSet of J st A cc= B & B cc= A holds

A = B

let B be ManySortedSet of J; :: thesis: ( A cc= B & B cc= A implies A = B )

assume that

A1: A cc= B and

A2: B cc= A ; :: thesis: A = B

A3: I c= J by A1;

J c= I by A2;

then I = J by A3, XBOOLE_0:def 10;

then reconsider B9 = B as ManySortedSet of I ;

now :: thesis: for i being object st i in I holds

A . i = B9 . i

hence
A = B
by PBOOLE:3; :: thesis: verumA . i = B9 . i

let i be object ; :: thesis: ( i in I implies A . i = B9 . i )

assume i in I ; :: thesis: A . i = B9 . i

then ( A . i c= B . i & B . i c= A . i ) by A1, A2;

hence A . i = B9 . i by XBOOLE_0:def 10; :: thesis: verum

end;assume i in I ; :: thesis: A . i = B9 . i

then ( A . i c= B . i & B . i c= A . i ) by A1, A2;

hence A . i = B9 . i by XBOOLE_0:def 10; :: thesis: verum