theorem :: BINOP_2:1

the_unity_wrt addcomplex = 0 by Lm1, NUMBERS:20, Lm2, BINOP_1:def 8;