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