let z be Element of F_Complex; :: thesis: ( z <> 0. F_Complex implies (z ") *' = (z *') " )
reconsider z1 = z as Element of COMPLEX by Def1;
assume A1: z <> 0. F_Complex ; :: thesis: (z ") *' = (z *') "
then A2: z *' <> 0. F_Complex by Th84;
z " = z1 " by A1, Th7;
hence (z ") *' = (z1 *') " by COMPLEX1:36
.= (z *') " by A2, Th7 ;
:: thesis: verum