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