let n be Nat; :: thesis: for z, z1 being Element of COMPLEX n holds z1 = (z1 + z) - z
let z, z1 be Element of COMPLEX n; :: thesis: z1 = (z1 + z) - z
thus z1 = z1 + (0c n) by BINOP_2:1, FINSEQOP:56
.= z1 + (z - z) by Th72
.= (z1 + z) - z by Th75 ; :: thesis: verum