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