theorem :: BINOP_2:4

the_unity_wrt addint = 0 by Lm1, NUMBERS:17, Lm5, BINOP_1:def 8;