let I be set ; :: thesis: for x, A, B, y, X, Y being ManySortedSet of I st x c= [|A,B|] & y c= [|X,Y|] holds
x \/ y c= [|(A \/ X),(B \/ Y)|]
let x, A, B, y, X, Y be ManySortedSet of I; :: thesis: ( x c= [|A,B|] & y c= [|X,Y|] implies x \/ y c= [|(A \/ X),(B \/ Y)|] )
assume A1: ( x c= [|A,B|] & y c= [|X,Y|] ) ; :: thesis: x \/ y c= [|(A \/ X),(B \/ Y)|]
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or (x \/ y) . i c= [|(A \/ X),(B \/ Y)|] . i )
assume A2: i in I ; :: thesis: (x \/ y) . i c= [|(A \/ X),(B \/ Y)|] . i
then ( x . i c= [|A,B|] . i & y . i c= [|X,Y|] . i ) by A1, PBOOLE:def 5;
then ( x . i c= [:(A . i),(B . i):] & y . i c= [:(X . i),(Y . i):] ) by A2, PBOOLE:def 21;
then (x . i) \/ (y . i) c= [:((A . i) \/ (X . i)),((B . i) \/ (Y . i)):] by ZFMISC_1:143;
then (x \/ y) . i c= [:((A . i) \/ (X . i)),((B . i) \/ (Y . i)):] by A2, PBOOLE:def 7;
then (x \/ y) . i c= [:((A \/ X) . i),((B . i) \/ (Y . i)):] by A2, PBOOLE:def 7;
then (x \/ y) . i c= [:((A \/ X) . i),((B \/ Y) . i):] by A2, PBOOLE:def 7;
hence (x \/ y) . i c= [|(A \/ X),(B \/ Y)|] . i by A2, PBOOLE:def 21; :: thesis: verum