the_unity_wrt multextreal = 1 by Lm1, BINOP_1:def 8;