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;
thus - (z1 / z2) = - (z19 / z29) by A1, Th6
.= (- z19) / z29 by XCMPLX_1:187
.= (- z1) / z2 by A1, Th6 ; :: thesis: - (z1 / z2) = z1 / (- z2)
thus - (z1 / z2) = - (z19 / z29) by A1, Th6
.= z19 / (- z29) by XCMPLX_1:188
.= z1 / (- z2) by A2, Th6 ; :: thesis: verum