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 Th33
.= {(f / h),(f / i),(g / h),(g / i)} by Th94 ; :: thesis: verum