theorem :: PZFMISC1:80

for I being set
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)|]