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 Th92
.= {(a * s),(a * t)} \/ ({b} ** {s,t}) by Th99
.= {(a * s),(a * t)} \/ {(b * s),(b * t)} by Th99
.= {(a * s),(a * t),(b * s),(b * t)} by ENUMSET1:5 ; :: thesis: verum