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