let a, b, s, t be Complex; {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
; verum