let n be Nat; for z1, z2 being Element of COMPLEX n holds - (z1 + z2) = (- z1) + (- z2)
let z1, z2 be Element of COMPLEX n; - (z1 + z2) = (- z1) + (- z2)
(z1 + z2) + ((- z1) + (- z2)) =
((z2 + z1) + (- z1)) + (- z2)
by FINSEQOP:28
.=
(z2 + (z1 + (- z1))) + (- z2)
by FINSEQOP:28
.=
(z2 + (0c n)) + (- z2)
by Th51, Th52, BINOP_2:1, FINSEQOP:73
.=
z2 + (- z2)
by BINOP_2:1, FINSEQOP:56
.=
0c n
by Th51, Th52, BINOP_2:1, FINSEQOP:73
;
hence
- (z1 + z2) = (- z1) + (- z2)
by Th51, Th52, BINOP_2:1, FINSEQOP:74; verum