:: deftheorem Def6 defines DigitSD RADIX_1:def 6 :
for n, k being Nat
for x being Tuple of n,k -SD
for b₄ being Tuple of n, INT holds
( b₄ = DigitSD x iff for i being Nat st i in Seg n holds
b₄ /. i = SubDigit (x,i,k) );