theorem :: BINOP_2:8

the_unity_wrt multrat = 1 by Lm7, NUMBERS:18, Lm10, BINOP_1:def 8;