theorem :: BINOP_2:9

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