let n be Element of NAT ; :: thesis: for z being Element of COMPLEX n holds z - z = 0c n
let z be Element of COMPLEX n; :: thesis: z - z = 0c n
thus z - z = z + (- z)
.= 0c n by Th7, Th8, BINOP_2:1, FINSEQOP:77 ; :: thesis: verum