:: deftheorem Def1 defines multextreal MESFUNC7:def 1 :
for b₁ being BinOp of ExtREAL holds
( b₁ = multextreal iff for x, y being Element of ExtREAL holds b₁ . (x,y) = x * y );