let n be 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 Th51, Th52, BINOP_2:1, FINSEQOP:73 ; :: thesis: verum