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