let f, g, h be ext-real number ; :: thesis: {f} ++ {g,h} = {(f + g),(f + h)}
thus {f} ++ {g,h} = {f} ++ ({g} \/ {h}) by ENUMSET1:41
.= ({f} ++ {g}) \/ ({f} ++ {h}) by Th47
.= {(f + g)} \/ ({f} ++ {h}) by Th49
.= {(f + g)} \/ {(f + h)} by Th49
.= {(f + g),(f + h)} by ENUMSET1:41 ; :: thesis: verum