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