theorem Th45: :: MEMBER_1:45
for f, g, h, i being ExtReal holds {f,g} ++ {h,i} = {(f + h),(f + i),(g + h),(g + i)}