let f, g, h be ExtReal; :: thesis: {f} ++ {g,h} = {(f + g),(f + h)}
thus {f} ++ {g,h} = {f} ++ ({g} \/ {h}) by ENUMSET1:1
.= ({f} ++ {g}) \/ ({f} ++ {h}) by Th41
.= {(f + g)} \/ ({f} ++ {h}) by Th43
.= {(f + g)} \/ {(f + h)} by Th43
.= {(f + g),(f + h)} by ENUMSET1:1 ; :: thesis: verum