theorem Th19: :: NUMERAL2:19
for n, b being Nat st b > 1 holds
n = (b * (value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b))) + ((digits (n,b)) . 0)