:: deftheorem Def1 defines MODMAP_ LAGRA4SQ:def 2 :
for p being odd prime Nat
for b₂ being Function of INT,(Segm p) holds
( b₂ = MODMAP_ p iff for x being Element of INT holds b₂ . x = x mod p );