theorem Th73: :: COHSP_1:73

for x, y being set holds x U+ y = [:x,{1}:] \/ [:y,{2}:]