let a, b be Complex; :: thesis: a / (1 / b) = a * b
thus a / (1 / b) = a / (b ") by Lm4
.= a * (1 / (b ")) by Lm14
.= a * b by Lm16 ; :: thesis: verum