let n, k be Nat; :: thesis: for b being non trivial Nat holds (digits (n,b)) . k < b
let b be non trivial Nat; :: thesis: (digits (n,b)) . k < b
A1: b > 1 by NEWTON03:def 1;
reconsider x = digits (n,b) as XFinSequence of NAT ;

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

suppose n = 0 ; :: thesis: (digits (n,b)) . k < b

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

end;

suppose B1: n <> 0 ; :: thesis: (digits (n,b)) . k < b

then reconsider n = n as non zero Nat ;

per cases ( k in dom x or not k in dom x ) ;

suppose k in dom x ; :: thesis: (digits (n,b)) . k < b

hence (digits (n,b)) . k < b by A1, B1, NUMERAL1:def 2; :: thesis: verum

end;

suppose not k in dom x ; :: thesis: (digits (n,b)) . k < b

hence (digits (n,b)) . k < b by FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

end;