theorem :: BINOP_2:6

the_unity_wrt multcomplex = 1 by Lm7, NUMBERS:20, Lm8, BINOP_1:def 8;