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 Th51, Th52, BINOP_2:1, FINSEQOP:73
.= (z1 + (- z)) + z by FINSEQOP:28
.= (z1 - z) + z ; :: thesis: verum