:: deftheorem defines mod AOFA_A00:def 48 :
for S being non empty non void 4,1 integer BoolSignature
for A being non-empty MSAlgebra over S
for I being integer SortSymbol of S
for a, b being Element of A,I holds a mod b = a + (- ((a div b) * b));