:: deftheorem Def2 defines SDMin RADIX_5:def 2 :
for n, m, k being Nat
for b₄ being Tuple of n,k -SD holds
( b₄ = SDMin (n,m,k) iff for i being Nat st i in Seg n holds
DigA (b₄,i) = SDMinDigit (m,k,i) );