theorem Th20: :: RADIX_1:21

for k, m being Nat st m is_represented_by 1,k holds
DigA ((DecSD (m,1,k)),1) = m