let a, b be complex number ; :: thesis: a / (1 / b) = a * b
thus a / (1 / b) = a / (b " ) by Lm4
.= a * (1 / (b " )) by Lm15
.= a * b by Lm17 ; :: thesis: verum