:: deftheorem Def3 defines mod INT_6:def 3 :
for u being Integer
for m being integer-valued FinSequence
for b₃ being FinSequence holds
( b₃ = mod (u,m) iff ( len b₃ = len m & ( for i being Nat st i in dom b₃ holds
b₃ . i = u mod (m . i) ) ) );