let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I holds
( [|(X (/\) Y),Z|] = [|X,Z|] (/\) [|Y,Z|] & [|Z,(X (/\) Y)|] = [|Z,X|] (/\) [|Z,Y|] )
let X, Y, Z be ManySortedSet of I; :: thesis: ( [|(X (/\) Y),Z|] = [|X,Z|] (/\) [|Y,Z|] & [|Z,(X (/\) Y)|] = [|Z,X|] (/\) [|Z,Y|] )

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

let i be object ; :: thesis: ( i in I implies [|(X (/\) Y),Z|] . i = ([|X,Z|] (/\) [|Y,Z|]) . i )
assume A1: i in I ; :: thesis: [|(X (/\) Y),Z|] . i = ([|X,Z|] (/\) [|Y,Z|]) . i
hence [|(X (/\) Y),Z|] . i = [:((X (/\) Y) . i),(Z . i):] by PBOOLE:def 16
.= [:((X . i) /\ (Y . i)),(Z . i):] by A1, PBOOLE:def 5
.= [:(X . i),(Z . i):] /\ [:(Y . i),(Z . i):] by ZFMISC_1:99
.= ([|X,Z|] . i) /\ [:(Y . i),(Z . i):] by A1, PBOOLE:def 16
.= ([|X,Z|] . i) /\ ([|Y,Z|] . i) by A1, PBOOLE:def 16
.= ([|X,Z|] (/\) [|Y,Z|]) . i by A1, PBOOLE:def 5 ;
:: thesis: verum

end;

hence [|(X (/\) Y),Z|] = [|X,Z|] (/\) [|Y,Z|] ; :: thesis: [|Z,(X (/\) Y)|] = [|Z,X|] (/\) [|Z,Y|]

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

let i be object ; :: thesis: ( i in I implies [|Z,(X (/\) Y)|] . i = ([|Z,X|] (/\) [|Z,Y|]) . i )
assume A2: i in I ; :: thesis: [|Z,(X (/\) Y)|] . i = ([|Z,X|] (/\) [|Z,Y|]) . i
hence [|Z,(X (/\) Y)|] . i = [:(Z . i),((X (/\) Y) . i):] by PBOOLE:def 16
.= [:(Z . i),((X . i) /\ (Y . i)):] by A2, PBOOLE:def 5
.= [:(Z . i),(X . i):] /\ [:(Z . i),(Y . i):] by ZFMISC_1:99
.= ([|Z,X|] . i) /\ [:(Z . i),(Y . i):] by A2, PBOOLE:def 16
.= ([|Z,X|] . i) /\ ([|Z,Y|] . i) by A2, PBOOLE:def 16
.= ([|Z,X|] (/\) [|Z,Y|]) . i by A2, PBOOLE:def 5 ;
:: thesis: verum

end;

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