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:36; :: 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 4;
hence len (digits n,b) >= 1 by NAT_1:14; :: thesis: verum

end;

end;