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