theorem Th5: :: MESFUNC7:5

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