theorem Th12: :: RADIX_2:12

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