:: deftheorem defines SDDec2 RADIX_2:def 3 :
for n, k being Nat
for x being Tuple of n, NAT holds SDDec2 (x,k) = Sum (DigitSD2 (x,k));