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