theorem Th14: :: RADIX_2:14

for x, n, k being Nat holds DecSD2 (x,n,k) = DecSD (x,n,k)