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

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

suppose n = 0 ; :: thesis: len (digits (n,b)) >= 1

then digits (n,b) = <%0%> by A1, Def2;
hence len (digits (n,b)) >= 1 by AFINSQ_1:33; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: len (digits (n,b)) >= 1

then (digits (n,b)) . ((len (digits (n,b))) - 1) <> 0 by A1, Def2;
then (len (digits (n,b))) - 1 in dom (digits (n,b)) by FUNCT_1:def 2;
hence len (digits (n,b)) >= 1 by NAT_1:14; :: thesis: verum

end;

end;