let a, b, s be complex number ; :: thesis: {a,b} /// {s} = {(a / s),(b / s)}
thus {a,b} /// {s} = {a,b} ** {(s " )} by Th43
.= {(a / s),(b / s)} by Th105 ; :: thesis: verum