let n be Nat; :: thesis: for b being non trivial Nat st n >= b holds
len (digits (n,b)) > 1
let b be non trivial Nat; :: thesis: ( n >= b implies len (digits (n,b)) > 1 )
assume A1: n >= b ; :: thesis: len (digits (n,b)) > 1
assume A2: not len (digits (n,b)) > 1 ; :: thesis: contradiction
A3: len (digits (n,b)) >= 1 by NUMERAL1:4, NEWTON03:def 1;
then A4: len (digits (n,b)) = 1 by A2, XXREAL_0:1;
A5: 0 in 1 by CARD_1:49, TARSKI:def 1;
consider x being XFinSequence of NAT such that
A6: ( dom x = dom (digits (n,b)) & ( for i being Nat st i in dom x holds
x . i = ((digits (n,b)) . i) * (b |^ i) ) & value ((digits (n,b)),b) = Sum x ) by NUMERAL1:def 1;
reconsider f = x as 1 -element complex-valued XFinSequence by A2, A3, XXREAL_0:1, A6, CARD_1:def 7;
n = Sum (x | (dom x)) by A6
.= x . 0 by A4, A6, RVSUM_4:48
.= ((digits (n,b)) . 0) * (b |^ 0) by A4, A6, A5
.= ((digits (n,b)) . 0) * 1 by NEWTON:4 ;
then digits (n,b) = <%n%> by A4, AFINSQ_1:def 4;
hence contradiction by A1, Th26; :: thesis: verum