theorem Th9: :: NUMBER11:9

for n, b being Nat st b > 1 holds
n < b |^ (len (digits (n,b)))