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