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

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

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

hence digits (n,b) = <%n%> by A1, NUMERAL1:def 2; :: thesis: verum

end;

suppose A2: n > 0 ; :: thesis: digits (n,b) = <%n%>

A3: value (<%n%>,b) = n by Th2;
len <%n%> = 1 by AFINSQ_1:34;
then <%n%> . ((len <%n%>) - 1) = n ;
then A4: <%n%> . ((len <%n%>) - 1) <> 0 by A2;

now :: thesis: for i being Nat st i in dom <%n%> holds
( 0 <= <%n%> . i & <%n%> . i < b )

let i be Nat; :: thesis: ( i in dom <%n%> implies ( 0 <= <%n%> . i & <%n%> . i < b ) )
assume i in dom <%n%> ; :: thesis: ( 0 <= <%n%> . i & <%n%> . i < b )
then i in 1 by AFINSQ_1:def 4;
then i in {0} by CARD_1:49;
then i = 0 by TARSKI:def 1;
hence ( 0 <= <%n%> . i & <%n%> . i < b ) by A1; :: thesis: verum

end;

hence digits (n,b) = <%n%> by A2, A1, A3, A4, NUMERAL1:def 2; :: thesis: verum

end;

end;