for n, k being Nat
for x being Tuple of n, NAT
for y being Tuple of n,k -SD st x = y holds
DigitSD2 (x,k) = DigitSD y