:: deftheorem Def4 defines mod AOFA_I00:def 4 :
for t1, t2, b₃ being INT -valued Function holds
( b₃ = t1 mod t2 iff ( dom b₃ = (dom t1) /\ (dom t2) & ( for s being object st s in dom b₃ holds
b₃ . s = (t1 . s) mod (t2 . s) ) ) );