theorem Th15: :: RADIX_2:15

for n being Nat st n >= 1 holds
for m, k being Nat st m is_represented_by n,k holds
m = SDDec2 ((DecSD2 (m,n,k)),k)