theorem :: BINOP_2:3

the_unity_wrt addrat = 0 by Lm1, NUMBERS:18, Lm4, BINOP_1:def 8;