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