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