theorem :: BINOP_2:7

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