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