theorem Th4: :: RADIX_5:4

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