let a be Complex; :: thesis: ( a <> 0 implies a * (1 / a) = 1 )
assume A1: a <> 0 ; :: thesis: a * (1 / a) = 1
thus a * (1 / a) = a * (a ") by Lm4
.= 1 by A1, XCMPLX_0:def 7 ; :: thesis: verum