let I be set ; :: thesis: for x1, x2, A, B being ManySortedSet of holds [|(x1 \/ x2),(A \/ B)|] = (([|x1,A|] \/ [|x1,B|]) \/ [|x2,A|]) \/ [|x2,B|]
let x1, x2, A, B be ManySortedSet of ; :: 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|]) . ihence [|(x1 \/ x2),(A \/ B)|] . i =
[:((x1 \/ x2) . i),((A \/ B) . i):]
by PBOOLE:def 21
.=
[:((x1 . i) \/ (x2 . i)),((A \/ B) . i):]
by A1, PBOOLE:def 7
.=
[:((x1 . i) \/ (x2 . i)),((A . i) \/ (B . i)):]
by A1, PBOOLE:def 7
.=
(([:(x1 . i),(A . i):] \/ [:(x1 . i),(B . i):]) \/ [:(x2 . i),(A . i):]) \/ [:(x2 . i),(B . i):]
by ZFMISC_1:121
.=
((([|x1,A|] . i) \/ [:(x1 . i),(B . i):]) \/ [:(x2 . i),(A . i):]) \/ [:(x2 . i),(B . i):]
by A1, PBOOLE:def 21
.=
((([|x1,A|] . i) \/ ([|x1,B|] . i)) \/ [:(x2 . i),(A . i):]) \/ [:(x2 . i),(B . i):]
by A1, PBOOLE:def 21
.=
((([|x1,A|] . i) \/ ([|x1,B|] . i)) \/ ([|x2,A|] . i)) \/ [:(x2 . i),(B . i):]
by A1, PBOOLE:def 21
.=
((([|x1,A|] . i) \/ ([|x1,B|] . i)) \/ ([|x2,A|] . i)) \/ ([|x2,B|] . i)
by A1, PBOOLE:def 21
.=
((([|x1,A|] \/ [|x1,B|]) . i) \/ ([|x2,A|] . i)) \/ ([|x2,B|] . i)
by A1, PBOOLE:def 7
.=
((([|x1,A|] \/ [|x1,B|]) \/ [|x2,A|]) . i) \/ ([|x2,B|] . i)
by A1, PBOOLE:def 7
.=
((([|x1,A|] \/ [|x1,B|]) \/ [|x2,A|]) \/ [|x2,B|]) . i
by A1, PBOOLE:def 7
;
:: thesis: verum end;
hence
[|(x1 \/ x2),(A \/ B)|] = (([|x1,A|] \/ [|x1,B|]) \/ [|x2,A|]) \/ [|x2,B|]
by PBOOLE:3; :: thesis: verum