let a, s, t be Complex; :: thesis: {a} ++ {s,t} = {(a + s),(a + t)}
thus {a} ++ {s,t} = {a} ++ ({s} \/ {t}) by ENUMSET1:1
.= ({a} ++ {s}) \/ ({a} ++ {t}) by Th48
.= {(a + s)} \/ ({a} ++ {t}) by Th51
.= {(a + s)} \/ {(a + t)} by Th51
.= {(a + s),(a + t)} by ENUMSET1:1 ; :: thesis: verum