let n be Element of NAT ; :: thesis: for z1, z being Element of COMPLEX n holds z1 = (z1 + z) - z
let z1, z 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 Th90
.= (z1 + z) - z by Th93 ; :: thesis: verum