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