let a be complex number ; :: thesis: 1 / (a ") = a
1 / (a ") = (a ") " by Lm4
.= a ;
hence 1 / (a ") = a ; :: thesis: verum