:: deftheorem Def10 defines multint INT_3:def 10 :
for n being natural Number st n > 0 holds
for b₂ being BinOp of (Segm n) holds
( b₂ = multint n iff for k, l being Element of Segm n holds b₂ . (k,l) = (k * l) mod n );