let n be Nat; :: thesis: for b being non trivial Nat st digits (n,b) = <%n%> holds
n < b
let b be non trivial Nat; :: thesis: ( digits (n,b) = <%n%> implies n < b )
A1: b > 1 by NEWTON03:def 1;
assume A2: digits (n,b) = <%n%> ; :: thesis: n < b
then A3: ( len (digits (n,b)) = 1 & (digits (n,b)) . 0 = n ) by AFINSQ_1:def 4;

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

suppose n = 0 ; :: thesis: n < b

hence n < b ; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: n < b

then reconsider n = n as non zero Nat ;
0 in dom <%n%> by A2, A3, CARD_1:49, TARSKI:def 1;
hence n < b by A1, A2, A3, NUMERAL1:def 2; :: thesis: verum

end;

end;