theorem :: BINOP_2:10

the_unity_wrt multnat = 1 by Lm12, BINOP_1:def 8;