theorem Th10: :: NUMBER11:10
for n, m, b being Nat st n <> 0 & b > 1 & m < len (digits (n,b)) holds
n >= b |^ m