theorem Th81: :: COHSP_1:81

for x1, y1, x2, y2 being set holds (x1 U+ y1) \/ (x2 U+ y2) = (x1 \/ x2) U+ (y1 \/ y2)