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

proof

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

end;

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