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

let i be set ; :: 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|] by PBOOLE:3; :: thesis: verum