theorem Th13: :: RADIX_2:13

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