let n be Element of 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 Lm3
.= z by BINOP_2:1, FINSEQOP:57 ; :: thesis: verum