let n be Nat; :: thesis: for z1, z2 being Element of COMPLEX n holds - (z1 + z2) = (- z1) + (- z2)
let z1, z2 be Element of COMPLEX n; :: thesis: - (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; :: thesis: verum