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