:: deftheorem defines Table1 RADIX_2:def 6 :
for q being Integer
for f, j, k, n being Nat
for c being Tuple of n,k -SD holds Table1 (q,c,f,j) = (q * (DigA (c,j))) mod f;