theorem :: BINOP_2:5

the_unity_wrt addnat = 0 by Lm6, BINOP_1:def 8;