let n be Nat; :: thesis: - (0c n) = 0c n
thus - (0c n) = n |-> (compcomplex . 0c) by FINSEQOP:16
.= n |-> (- 0c) by BINOP_2:def 1
.= 0c n ; :: thesis: verum