theorem Th23: :: RADIX_1:24

for k, m, n being Nat st m is_represented_by n + 1,k holds
DigA ((DecSD (m,(n + 1),k)),(n + 1)) = m div ((Radix k) |^ n)