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 Th48;
z " = z1 " by A1, Th5;
hence (z ") *' = (z1 *') " by COMPLEX1:36
.= (z *') " by A2, Th5 ;
:: thesis: verum