theorem Th7: :: RADIX_2:7

for k being Nat
for x being Tuple of 1,k -SD holds SDDec x = DigA (x,1)