:: deftheorem Def5 defines DigA_SDSub RADIX_3:def 5 :
for i, k, n being Nat
for x being Tuple of n,k -SD_Sub holds
( ( i in Seg n implies DigA_SDSub (x,i) = x . i ) & ( i = 0 implies DigA_SDSub (x,i) = 0 ) );