let a, b be complex number ; :: 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 Lm8
.= (a * b) / a by Lm9
.= (a / a) * b by Lm9
.= 1 * b by A1, Lm5
.= b ; :: thesis: verum