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