:: deftheorem Def9 defines Pow_mod RADIX_2:def 9 :
for k, f, m, n being Nat
for e being Tuple of n, NAT st n >= 1 holds
for b₆ being Tuple of n, NAT holds
( b₆ = Pow_mod (m,e,f,k) iff ( b₆ . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex i1, i2 being Nat st
( i1 = b₆ . i & i2 = b₆ . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) ) );