:: deftheorem Def6 defines Mmin RADIX_6:def 6 :
for m, k being Nat
for r, b₄ being Tuple of m + 2,k -SD holds
( b₄ = Mmin r iff for i being Nat st i in Seg (m + 2) holds
DigA (b₄,i) = MminDigit (r,i) );