let n be Element of 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:29
.= (z2 + (z1 + (- z1))) + (- z2) by FINSEQOP:29
.= (z2 + (0c n)) + (- z2) by Th7, Th8, BINOP_2:1, FINSEQOP:77
.= z2 + (- z2) by BINOP_2:1, FINSEQOP:57
.= 0c n by Th7, Th8, BINOP_2:1, FINSEQOP:77 ;
hence - (z1 + z2) = (- z1) + (- z2) by Th7, Th8, BINOP_2:1, FINSEQOP:78; :: thesis: verum