:: deftheorem Def22 defines multint BINOP_2:def 22 :
for b₁ being BinOp of INT holds
( b₁ = multint iff for i1, i2 being Integer holds b₁ . (i1,i2) = i1 * i2 );