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