let I be set ; :: thesis: for x1, x2, A, B being ManySortedSet of I st ( x1 /\ x2 = [[0]] I or A /\ B = [[0]] I ) holds
[|x1,A|] /\ [|x2,B|] = [[0]] I
let x1, x2, A, B be ManySortedSet of I; :: thesis: ( ( x1 /\ x2 = [[0]] I or A /\ B = [[0]] I ) implies [|x1,A|] /\ [|x2,B|] = [[0]] I )
assume A1: ( x1 /\ x2 = [[0]] I or A /\ B = [[0]] I ) ; :: thesis: [|x1,A|] /\ [|x2,B|] = [[0]] I

per cases ( x1 /\ x2 = [[0]] I or A /\ B = [[0]] I ) by A1;

suppose A2: x1 /\ x2 = [[0]] I ; :: thesis: [|x1,A|] /\ [|x2,B|] = [[0]] I

now

let i be set ; :: thesis: ( i in I implies ([|x1,A|] /\ [|x2,B|]) . i = ([[0]] I) . i )
assume A3: i in I ; :: thesis: ([|x1,A|] /\ [|x2,B|]) . i = ([[0]] I) . i
then (x1 . i) /\ (x2 . i) = (x1 /\ x2) . i by PBOOLE:def 5
.= {} by A2, PBOOLE:5 ;
then x1 . i misses x2 . i by XBOOLE_0:def 7;
then A4: [:(x1 . i),(A . i):] misses [:(x2 . i),(B . i):] by ZFMISC_1:104;
thus ([|x1,A|] /\ [|x2,B|]) . i = ([|x1,A|] . i) /\ ([|x2,B|] . i) by A3, PBOOLE:def 5
.= [:(x1 . i),(A . i):] /\ ([|x2,B|] . i) by A3, PBOOLE:def 16
.= [:(x1 . i),(A . i):] /\ [:(x2 . i),(B . i):] by A3, PBOOLE:def 16
.= {} by A4, XBOOLE_0:def 7
.= ([[0]] I) . i by PBOOLE:5 ; :: thesis: verum

end;

hence [|x1,A|] /\ [|x2,B|] = [[0]] I by PBOOLE:3; :: thesis: verum

end;

suppose A5: A /\ B = [[0]] I ; :: thesis: [|x1,A|] /\ [|x2,B|] = [[0]] I

now

let i be set ; :: thesis: ( i in I implies ([|x1,A|] /\ [|x2,B|]) . i = ([[0]] I) . i )
assume A6: i in I ; :: thesis: ([|x1,A|] /\ [|x2,B|]) . i = ([[0]] I) . i
then (A . i) /\ (B . i) = (A /\ B) . i by PBOOLE:def 5
.= {} by A5, PBOOLE:5 ;
then A . i misses B . i by XBOOLE_0:def 7;
then A7: [:(x1 . i),(A . i):] misses [:(x2 . i),(B . i):] by ZFMISC_1:104;
thus ([|x1,A|] /\ [|x2,B|]) . i = ([|x1,A|] . i) /\ ([|x2,B|] . i) by A6, PBOOLE:def 5
.= [:(x1 . i),(A . i):] /\ ([|x2,B|] . i) by A6, PBOOLE:def 16
.= [:(x1 . i),(A . i):] /\ [:(x2 . i),(B . i):] by A6, PBOOLE:def 16
.= {} by A7, XBOOLE_0:def 7
.= ([[0]] I) . i by PBOOLE:5 ; :: thesis: verum

end;

hence [|x1,A|] /\ [|x2,B|] = [[0]] I by PBOOLE:3; :: thesis: verum

end;

end;