let a, b, s be Complex; :: thesis: {a,b} /// {s} = {(a / s),(b / s)}
thus {a,b} /// {s} = {a,b} ** {(s ")} by Th37
.= {(a / s),(b / s)} by Th99 ; :: thesis: verum