:: deftheorem Def7 defines FmaxDigit RADIX_5:def 7 :
for i, m, k being Nat st k >= 2 holds
( ( i = m implies FmaxDigit (m,k,i) = (Radix k) - 1 ) & ( not i = m implies FmaxDigit (m,k,i) = 0 ) );