:: deftheorem Def7 defines Mul_mod RADIX_2:def 7 :
for q being Integer
for k, f, n being Nat
for c being Tuple of n,k -SD st n >= 1 holds
for b₆ being Tuple of n, INT holds
( b₆ = Mul_mod (q,c,f,k) iff ( b₆ . 1 = Table1 (q,c,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex I1, I2 being Integer st
( I1 = b₆ . i & I2 = b₆ . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ) ) );