:: deftheorem Def4 defines addint GR_CY_1:def 4 :
for n being natural Number st n > 0 holds
for b₂ being BinOp of (Segm n) holds
( b₂ = addint n iff for k, l being Element of Segm n holds b₂ . (k,l) = (k + l) mod n );