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