let I be set ; :: thesis: for A, B, X, Y being ManySortedSet of I st A c= X & B c= Y holds
[|A,Y|] (/\) [|X,B|] = [|A,B|]
let A, B, X, Y be ManySortedSet of I; :: thesis: ( A c= X & B c= Y implies [|A,Y|] (/\) [|X,B|] = [|A,B|] )
assume that
A1: A c= X and
A2: B c= Y ; :: thesis: [|A,Y|] (/\) [|X,B|] = [|A,B|]

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

let i be object ; :: thesis: ( i in I implies ([|A,Y|] (/\) [|X,B|]) . i = [|A,B|] . i )
assume A3: i in I ; :: thesis: ([|A,Y|] (/\) [|X,B|]) . i = [|A,B|] . i
then A4: A . i c= X . i by A1;
A5: B . i c= Y . i by A2, A3;
thus ([|A,Y|] (/\) [|X,B|]) . i = ([|A,Y|] . i) /\ ([|X,B|] . i) by A3, PBOOLE:def 5
.= [:(A . i),(Y . i):] /\ ([|X,B|] . i) by A3, PBOOLE:def 16
.= [:(A . i),(Y . i):] /\ [:(X . i),(B . i):] by A3, PBOOLE:def 16
.= [:(A . i),(B . i):] by A4, A5, ZFMISC_1:101
.= [|A,B|] . i by A3, PBOOLE:def 16 ; :: thesis: verum

end;

hence [|A,Y|] (/\) [|X,B|] = [|A,B|] ; :: thesis: verum