let a be Complex; :: thesis: 1 / (1 / a) = a
thus 1 / (1 / a) = (1 * a) / 1 by Lm2
.= a ; :: thesis: verum