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;
assume A1: z <> 0. F_Complex ; :: thesis: z " = (1. F_Complex ) / z
A2: 1. F_Complex = 1r by Def1;
thus z " = z1 " by A1, Th7
.= 1r / z1 by XCMPLX_1:217
.= (1. F_Complex ) / z by A1, A2, Th8 ; :: thesis: verum