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