let a, b be Complex; :: thesis: ( a <> 0 implies a / (a / b) = b )
assume A1: a <> 0 ; :: thesis: a / (a / b) = b
thus a / (a / b) = a * ((a / b) ") by XCMPLX_0:def 9
.= a * (b / a) by Lm7
.= (a * b) / a by Lm8
.= (a / a) * b by Lm8
.= 1 * b by A1, Lm5
.= b ; :: thesis: verum