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:122
.= (z *' ) " by A2, Th7 ;
:: thesis: verum