:: deftheorem Def5 defines MminDigit RADIX_6:def 5 :
for i, m, k being Nat
for r being Tuple of m + 2,k -SD st k >= 2 & i in Seg (m + 2) holds
( ( i >= m implies MminDigit (r,i) = r . i ) & ( not i >= m implies MminDigit (r,i) = (- (Radix k)) + 1 ) );