let I be set ; :: thesis: for x, y, A, B, 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, y, A, B, 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 object ; :: according to PBOOLE:def 2 :: 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;
A5: y . i c= [|X,Y|] . i by A2, A3;
A6: x . i c= [:(A . i),(B . i):] by A3, A4, PBOOLE:def 16;
y . i c= [:(X . i),(Y . i):] by A3, A5, PBOOLE:def 16;
then (x . i) \/ (y . i) c= [:((A . i) \/ (X . i)),((B . i) \/ (Y . i)):] by A6, ZFMISC_1:119;
then (x (\/) y) . i c= [:((A . i) \/ (X . i)),((B . i) \/ (Y . i)):] by A3, PBOOLE:def 4;
then (x (\/) y) . i c= [:((A (\/) X) . i),((B . i) \/ (Y . i)):] by A3, PBOOLE:def 4;
then (x (\/) y) . i c= [:((A (\/) X) . i),((B (\/) Y) . i):] by A3, PBOOLE:def 4;
hence (x (\/) y) . i c= [|(A (\/) X),(B (\/) Y)|] . i by A3, PBOOLE:def 16; :: thesis: verum