:: deftheorem Def1 defines mod EULER_2:def 1 :
for f being integer-valued Function
for m being Integer
for b₃ being Function holds
( b₃ = f mod m iff ( dom b₃ = dom f & ( for i being object st i in dom f holds
b₃ . i = (f . i) mod m ) ) );