theorem :: BINOP_2:2

the_unity_wrt addreal = 0 by Lm3, BINOP_1:def 8;