let f, h, i be ext-real number ; :: thesis: {f} /// {h,i} = {(f / h),(f / i)}
thus {f} /// {h,i} = {f} ** {(h " ),(i " )} by Th27
.= {(f / h),(f / i)} by Th87 ; :: thesis: verum