:: deftheorem Def5 defines FminDigit RADIX_5:def 5 :
for i, m, k being Nat st k >= 2 holds
( ( i = m implies FminDigit (m,k,i) = 1 ) & ( not i = m implies FminDigit (m,k,i) = 0 ) );