theorem :: RADIX_3:21

for n being Nat st n >= 1 holds
for k, x being Nat st k >= 2 & x is_represented_by n,k holds
x = SDSub2IntOut (SD2SDSub (DecSD (x,n,k)))