theorem :: BINOP_2:4

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