:: deftheorem defines Table2 RADIX_2:def 8 :
for n, f, j, m being Nat
for e being Tuple of n, NAT holds Table2 (m,e,f,j) = (m |^ (e /. j)) mod f;