let f, h, i be ExtReal; :: thesis: {f} ** {h,i} = {(f * h),(f * i)}
thus {f} ** {h,i} = {f} ** ({h} \/ {i}) by ENUMSET1:1
.= ({f} ** {h}) \/ ({f} ** {i}) by Th82
.= {(f * h)} \/ ({f} ** {i}) by Th86
.= {(f * h)} \/ {(f * i)} by Th86
.= {(f * h),(f * i)} by ENUMSET1:1 ; :: thesis: verum