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