theorem Th5: :: ROUGHS_1:5

for D being set
for p, q being FinSequence of D holds Union (p ^ q) = (Union p) \/ (Union q)