let I be set ; :: thesis: for x1, x2, A, B being ManySortedSet of I holds [|x1,x2|] (\) [|A,B|] = [|(x1 (\) A),x2|] (\/) [|x1,(x2 (\) B)|]
let x1, x2, A, B be ManySortedSet of I; :: thesis: [|x1,x2|] (\) [|A,B|] = [|(x1 (\) A),x2|] (\/) [|x1,(x2 (\) B)|]
now :: thesis: for i being object st i in I holds
([|x1,x2|] (\) [|A,B|]) . i = ([|(x1 (\) A),x2|] (\/) [|x1,(x2 (\) B)|]) . i
let i be object ; :: thesis: ( i in I implies ([|x1,x2|] (\) [|A,B|]) . i = ([|(x1 (\) A),x2|] (\/) [|x1,(x2 (\) B)|]) . i )
assume A1: i in I ; :: thesis: ([|x1,x2|] (\) [|A,B|]) . i = ([|(x1 (\) A),x2|] (\/) [|x1,(x2 (\) B)|]) . i
hence ([|x1,x2|] (\) [|A,B|]) . i = ([|x1,x2|] . i) \ ([|A,B|] . i) by PBOOLE:def 6
.= [:(x1 . i),(x2 . i):] \ ([|A,B|] . i) by A1, PBOOLE:def 16
.= [:(x1 . i),(x2 . i):] \ [:(A . i),(B . i):] by A1, PBOOLE:def 16
.= [:((x1 . i) \ (A . i)),(x2 . i):] \/ [:(x1 . i),((x2 . i) \ (B . i)):] by ZFMISC_1:103
.= [:((x1 (\) A) . i),(x2 . i):] \/ [:(x1 . i),((x2 . i) \ (B . i)):] by A1, PBOOLE:def 6
.= [:((x1 (\) A) . i),(x2 . i):] \/ [:(x1 . i),((x2 (\) B) . i):] by A1, PBOOLE:def 6
.= ([|(x1 (\) A),x2|] . i) \/ [:(x1 . i),((x2 (\) B) . i):] by A1, PBOOLE:def 16
.= ([|(x1 (\) A),x2|] . i) \/ ([|x1,(x2 (\) B)|] . i) by A1, PBOOLE:def 16
.= ([|(x1 (\) A),x2|] (\/) [|x1,(x2 (\) B)|]) . i by A1, PBOOLE:def 4 ;
:: thesis: verum
end;
hence [|x1,x2|] (\) [|A,B|] = [|(x1 (\) A),x2|] (\/) [|x1,(x2 (\) B)|] ; :: thesis: verum