let z2, z1 be Element of F_Complex ; :: thesis: ( z2 <> 0. F_Complex implies ( - (z1 / z2) = (- z1) / z2 & - (z1 / z2) = z1 / (- z2) ) )
reconsider z1' = z1, z2' = z2 as Element of COMPLEX by Def1;
A1: - z1 = - z1' by Th4;
A2: - z2 = - z2' by Th4;
assume A3: z2 <> 0. F_Complex ; :: thesis: ( - (z1 / z2) = (- z1) / z2 & - (z1 / z2) = z1 / (- z2) )
then A4: - z2 <> 0. F_Complex by VECTSP_1:86;
z1 / z2 = z1' / z2' by A3, Th8;
hence - (z1 / z2) = - (z1' / z2') by Th4
.= (- z1') / z2' by XCMPLX_1:188
.= (- z1) / z2 by A1, A3, Th8 ;
:: thesis: - (z1 / z2) = z1 / (- z2)
z1 / z2 = z1' / z2' by A3, Th8;
hence - (z1 / z2) = - (z1' / z2') by Th4
.= z1' / (- z2') by XCMPLX_1:189
.= z1 / (- z2) by A2, A4, Th8 ;
:: thesis: verum