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
thus z1 + (z2 - z1) = (z2 + (- z1)) + z1
.= z2 + ((- z1) + z1) by FINSEQOP:28
.= z2 + (0c n) by Th51, Th52, BINOP_2:1, FINSEQOP:73
.= z2 by BINOP_2:1, FINSEQOP:56 ; :: thesis: verum