:: deftheorem defines SDSub2IntOut RADIX_3:def 12 :
for n, k being Nat
for x being Tuple of n,k -SD_Sub holds SDSub2IntOut x = Sum (SDSub2INT x);