let z2, z1 be Element of F_Complex ; :: thesis: ( z2 <> 0. F_Complex implies z1 / (z2 " ) = z1 * z2 )
reconsider z1' = z1, z2' = z2 as Element of COMPLEX by Def1;
assume A1: z2 <> 0. F_Complex ; :: thesis: z1 / (z2 " ) = z1 * z2
then A2: z2 " <> 0. F_Complex by VECTSP_1:74;
z2 " = z2' " by A1, Th7;
hence z1 / (z2 " ) = z1' / (z2' " ) by A2, Th8
.= z1 * z2 by XCMPLX_1:221 ;
:: thesis: verum