theorem Th9: :: SETLIM_2:9

for X being set
for A1, A2 being SetSequence of X holds Union (A1 (\/) A2) = (Union A1) \/ (Union A2)