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