let a, b be Complex; :: 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