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 that
A1: x c= [|A,B|] and
A2: 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 A3: i in I ; :: thesis: (x \/ y) . i c= [|(A \/ X),(B \/ Y)|] . i
then A4: x . i c= [|A,B|] . i by A1, PBOOLE:def 5;
A5: y . i c= [|X,Y|] . i by A2, A3, PBOOLE:def 5;
A6: x . i c= [:(A . i),(B . i):] by A3, A4, PBOOLE:def 21;
y . i c= [:(X . i),(Y . i):] by A3, A5, PBOOLE:def 21;
then (x . i) \/ (y . i) c= [:((A . i) \/ (X . i)),((B . i) \/ (Y . i)):] by A6, ZFMISC_1:143;
then (x \/ y) . i c= [:((A . i) \/ (X . i)),((B . i) \/ (Y . i)):] by A3, PBOOLE:def 7;
then (x \/ y) . i c= [:((A \/ X) . i),((B . i) \/ (Y . i)):] by A3, PBOOLE:def 7;
then (x \/ y) . i c= [:((A \/ X) . i),((B \/ Y) . i):] by A3, PBOOLE:def 7;
hence (x \/ y) . i c= [|(A \/ X),(B \/ Y)|] . i by A3, PBOOLE:def 21; :: thesis: verum