let a, b, s, t be complex number ; :: thesis: {a,b} ** {s,t} = {(a * s),(a * t),(b * s),(b * t)}
thus {a,b} ** {s,t} = ({a} \/ {b}) ** {s,t} by ENUMSET1:41
.= ({a} ** {s,t}) \/ ({b} ** {s,t}) by Th98
.= {(a * s),(a * t)} \/ ({b} ** {s,t}) by Th105
.= {(a * s),(a * t)} \/ {(b * s),(b * t)} by Th105
.= {(a * s),(a * t),(b * s),(b * t)} by ENUMSET1:45 ; :: thesis: verum