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