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

per cases ( X = EmptyMS I or Y = EmptyMS I ) by A1;

suppose A2: X = EmptyMS I ; :: thesis: [|X,Y|] = EmptyMS I

now :: thesis: for i being object st i in I holds
[|X,Y|] . i = (EmptyMS I) . i

let i be object ; :: thesis: ( i in I implies [|X,Y|] . i = (EmptyMS I) . i )
assume A3: i in I ; :: thesis: [|X,Y|] . i = (EmptyMS I) . i
A4: X . i = {} by A2, PBOOLE:5;
thus [|X,Y|] . i = [:(X . i),(Y . i):] by A3, PBOOLE:def 16
.= {} by A4, ZFMISC_1:90
.= (EmptyMS I) . i by PBOOLE:5 ; :: thesis: verum

end;

hence [|X,Y|] = EmptyMS I ; :: thesis: verum

end;

suppose A5: Y = EmptyMS I ; :: thesis: [|X,Y|] = EmptyMS I

now :: thesis: for i being object st i in I holds
[|X,Y|] . i = (EmptyMS I) . i

let i be object ; :: thesis: ( i in I implies [|X,Y|] . i = (EmptyMS I) . i )
assume A6: i in I ; :: thesis: [|X,Y|] . i = (EmptyMS I) . i
A7: Y . i = {} by A5, PBOOLE:5;
thus [|X,Y|] . i = [:(X . i),(Y . i):] by A6, PBOOLE:def 16
.= {} by A7, ZFMISC_1:90
.= (EmptyMS I) . i by PBOOLE:5 ; :: thesis: verum

end;

hence [|X,Y|] = EmptyMS I ; :: thesis: verum

end;

end;