theorem :: RADIX_2:16

for n being Nat st n >= 1 holds
for q being Integer
for ic, f, k being Nat st ic is_represented_by n,k & f > 0 holds
for c being Tuple of n,k -SD st c = DecSD (ic,n,k) holds
(Mul_mod (q,c,f,k)) . n = (q * ic) mod f