let n, b be Nat; :: thesis: ( b > 1 implies n < b |^ (len (digits (n,b))) )
assume A1: b > 1 ; :: thesis: n < b |^ (len (digits (n,b)))

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: n < b |^ (len (digits (n,b)))

hence n < b |^ (len (digits (n,b))) by A1; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: n < b |^ (len (digits (n,b)))

then A2: ( value ((digits (n,b)),b) = n & (digits (n,b)) . ((len (digits (n,b))) - 1) <> 0 & ( for i being Nat st i in dom (digits (n,b)) holds
( 0 <= (digits (n,b)) . i & (digits (n,b)) . i < b ) ) ) by NUMERAL1:def 2, A1;
A3: len (digits (n,b)) > 0 by NUMERAL1:4, A1;
for i being Nat st i in dom (digits (n,b)) holds
(digits (n,b)) . i < b by A2;
then value ((digits (n,b)),b) < b |^ (len (digits (n,b))) by A1, A3, Th8;
hence n < b |^ (len (digits (n,b))) by A2; :: thesis: verum

end;

end;