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

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

let i be object ; :: thesis: ( i in I implies [|(x1 (\/) x2),(A (\/) B)|] . i = ((([|x1,A|] (\/) [|x1,B|]) (\/) [|x2,A|]) (\/) [|x2,B|]) . i )
assume A1: i in I ; :: thesis: [|(x1 (\/) x2),(A (\/) B)|] . i = ((([|x1,A|] (\/) [|x1,B|]) (\/) [|x2,A|]) (\/) [|x2,B|]) . i
hence [|(x1 (\/) x2),(A (\/) B)|] . i = [:((x1 (\/) x2) . i),((A (\/) B) . i):] by PBOOLE:def 16
.= [:((x1 . i) \/ (x2 . i)),((A (\/) B) . i):] by A1, PBOOLE:def 4
.= [:((x1 . i) \/ (x2 . i)),((A . i) \/ (B . i)):] by A1, PBOOLE:def 4
.= (([:(x1 . i),(A . i):] \/ [:(x1 . i),(B . i):]) \/ [:(x2 . i),(A . i):]) \/ [:(x2 . i),(B . i):] by ZFMISC_1:98
.= ((([|x1,A|] . i) \/ [:(x1 . i),(B . i):]) \/ [:(x2 . i),(A . i):]) \/ [:(x2 . i),(B . i):] by A1, PBOOLE:def 16
.= ((([|x1,A|] . i) \/ ([|x1,B|] . i)) \/ [:(x2 . i),(A . i):]) \/ [:(x2 . i),(B . i):] by A1, PBOOLE:def 16
.= ((([|x1,A|] . i) \/ ([|x1,B|] . i)) \/ ([|x2,A|] . i)) \/ [:(x2 . i),(B . i):] by A1, PBOOLE:def 16
.= ((([|x1,A|] . i) \/ ([|x1,B|] . i)) \/ ([|x2,A|] . i)) \/ ([|x2,B|] . i) by A1, PBOOLE:def 16
.= ((([|x1,A|] (\/) [|x1,B|]) . i) \/ ([|x2,A|] . i)) \/ ([|x2,B|] . i) by A1, PBOOLE:def 4
.= ((([|x1,A|] (\/) [|x1,B|]) (\/) [|x2,A|]) . i) \/ ([|x2,B|] . i) by A1, PBOOLE:def 4
.= ((([|x1,A|] (\/) [|x1,B|]) (\/) [|x2,A|]) (\/) [|x2,B|]) . i by A1, PBOOLE:def 4 ;
:: thesis: verum

end;

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