:: deftheorem Def4 defines Mmax RADIX_6:def 4 :
for m, k being Nat
for r, b₄ being Tuple of m + 2,k -SD holds
( b₄ = Mmax r iff for i being Nat st i in Seg (m + 2) holds
DigA (b₄,i) = MmaxDigit (r,i) );