theorem :: BINOP_2:8

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