for n being Nat
for z being Element of COMPLEX n holds
( z + (- z) = 0c n & (- z) + z = 0c n ) by Th51, Th52, BINOP_2:1, FINSEQOP:73;