:: deftheorem defines SDDec RADIX_1:def 7 :
for n, k being Nat
for x being Tuple of n,k -SD holds SDDec x = Sum (DigitSD x);