:: deftheorem Def16 defines mult3 MOD_2:def 16 :
for b₁ being BinOp of {0,1,2} holds
( b₁ = mult3 iff for a, b being Element of {0,1,2} holds b₁ . (a,b) = a * b );