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