let z1, z2 be Element of F_Complex; :: thesis: ( z2 <> 0. F_Complex implies ( - (z1 / z2) = (- z1) / z2 & - (z1 / z2) = z1 / (- z2) ) )
assume A1: z2 <> 0. F_Complex ; :: thesis: ( - (z1 / z2) = (- z1) / z2 & - (z1 / z2) = z1 / (- z2) )
then A2: - z2 <> 0. F_Complex by VECTSP_1:28;
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
A3: - z1 = - z19 by Th2;
z1 / z2 = z19 / z29 by A1, Th6;
hence - (z1 / z2) = - (z19 / z29) by Th2
.= (- z19) / z29 by XCMPLX_1:187
.= (- z1) / z2 by A3, A1, Th6 ;
:: thesis: - (z1 / z2) = z1 / (- z2)
A4: - z2 = - z29 by Th2;
z1 / z2 = z19 / z29 by A1, Th6;
hence - (z1 / z2) = - (z19 / z29) by Th2
.= z19 / (- z29) by XCMPLX_1:188
.= z1 / (- z2) by A4, A2, Th6 ;
:: thesis: verum