let f, g, h be ExtReal; :: thesis: {f,g} /// {h} = {(f / h),(g / h)}
thus {f,g} /// {h} = {f,g} ** {(h ")} by Th26
.= {(f / h),(g / h)} by Th87 ; :: thesis: verum