let f, g, h, i be ext-real number ; :: thesis: {f,g} ** {h,i} = {(f * h),(f * i),(g * h),(g * i)}
thus {f,g} ** {h,i} = ({f} \/ {g}) ** {h,i} by ENUMSET1:41
.= ({f} ** {h,i}) \/ ({g} ** {h,i}) by Th88
.= {(f * h),(f * i)} \/ ({g} ** {h,i}) by Th93
.= {(f * h),(f * i)} \/ {(g * h),(g * i)} by Th93
.= {(f * h),(f * i),(g * h),(g * i)} by ENUMSET1:45 ; :: thesis: verum