theorem :: BINOP_2:9

the_unity_wrt multint = 1 by Lm7, NUMBERS:17, Lm11, BINOP_1:def 8;