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