let z be Element of F_Complex; :: thesis: ( z <> 0. F_Complex implies z / z = 1. F_Complex )
reconsider z1 = z as Element of COMPLEX by Def1;
assume A1: z <> 0. F_Complex ; :: thesis: z / z = 1. F_Complex
hence z / z = z1 / z1 by Th6
.= 1r by A1, Th7, XCMPLX_1:60
.= 1. F_Complex by Def1 ;
:: thesis: verum