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

per cases ( [|X,Z|] c= [|Y,Z|] or [|Z,X|] c= [|Z,Y|] ) by A2;

suppose A3: [|X,Z|] c= [|Y,Z|] ; :: thesis: X c= Y

let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or X . i c= Y . i )
assume A4: i in I ; :: thesis: X . i c= Y . i
then A5: not Z . i is empty by A1;
[|X,Z|] . i c= [|Y,Z|] . i by A3, A4;
then [:(X . i),(Z . i):] c= [|Y,Z|] . i by A4, PBOOLE:def 16;
then [:(X . i),(Z . i):] c= [:(Y . i),(Z . i):] by A4, PBOOLE:def 16;
hence X . i c= Y . i by A5, ZFMISC_1:94; :: thesis: verum

end;

suppose A6: [|Z,X|] c= [|Z,Y|] ; :: thesis: X c= Y

let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or X . i c= Y . i )
assume A7: i in I ; :: thesis: X . i c= Y . i
then A8: not Z . i is empty by A1;
[|Z,X|] . i c= [|Z,Y|] . i by A6, A7;
then [:(Z . i),(X . i):] c= [|Z,Y|] . i by A7, PBOOLE:def 16;
then [:(Z . i),(X . i):] c= [:(Z . i),(Y . i):] by A7, PBOOLE:def 16;
hence X . i c= Y . i by A8, ZFMISC_1:94; :: thesis: verum

end;

end;