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