theorem :: BINOP_2:7

the_unity_wrt multreal = 1 by Lm9, BINOP_1:def 8;