:: deftheorem Def11 defines SDSub2INT RADIX_3:def 11 :
for n, k being Nat
for x being Tuple of n,k -SD_Sub
for b₄ being Tuple of n, INT holds
( b₄ = SDSub2INT x iff for i being Nat st i in Seg n holds
b₄ /. i = SDSub2INTDigit (x,i,k) );