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

now

let i be set ; :: thesis: ( i in I implies [|(x1 /\ x2),(A /\ B)|] . i = ([|x1,A|] /\ [|x2,B|]) . i )
assume A1: i in I ; :: thesis: [|(x1 /\ x2),(A /\ B)|] . i = ([|x1,A|] /\ [|x2,B|]) . i
hence [|(x1 /\ x2),(A /\ B)|] . i = [:((x1 /\ x2) . i),((A /\ B) . i):] by PBOOLE:def 21
.= [:((x1 . i) /\ (x2 . i)),((A /\ B) . i):] by A1, PBOOLE:def 8
.= [:((x1 . i) /\ (x2 . i)),((A . i) /\ (B . i)):] by A1, PBOOLE:def 8
.= [:(x1 . i),(A . i):] /\ [:(x2 . i),(B . i):] by ZFMISC_1:123
.= ([|x1,A|] . i) /\ [:(x2 . i),(B . i):] by A1, PBOOLE:def 21
.= ([|x1,A|] . i) /\ ([|x2,B|] . i) by A1, PBOOLE:def 21
.= ([|x1,A|] /\ [|x2,B|]) . i by A1, PBOOLE:def 8 ;
:: thesis: verum

end;

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