let z1, z2 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 Th5, VECTSP_1:25;
hence z1 / (z2 ") = z19 / (z29 ") by Th6
.= z1 * z2 by XCMPLX_1:219 ;
:: thesis: verum