:: deftheorem Def8 defines SD2SDSub RADIX_3:def 8 :
for n, k being Nat
for x being Tuple of n,k -SD
for b₄ being Tuple of n + 1,k -SD_Sub holds
( b₄ = SD2SDSub x iff for i being Nat st i in Seg (n + 1) holds
DigA_SDSub (b₄,i) = SD2SDSubDigitS (x,i,k) );