:: deftheorem Def5 defines to_int INT_6:def 5 :
for u being INT -valued FinSequence
for m being CR_Sequence st len m = len u holds
for b₃ being Integer holds
( b₃ = to_int (u,m) iff for c being CR_coefficients of m holds b₃ = (Sum (u (#) c)) mod (Product m) );