let n, k, b be Nat; :: thesis: ( b > 1 & k > 0 & n > 0 implies digits (((k * (b |^ n)) + 1),b) = (<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b)) )
assume A1: ( b > 1 & k > 0 & n > 0 ) ; :: thesis: digits (((k * (b |^ n)) + 1),b) = (<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b))
set N = <%1%> ^ ((n -' 1) --> 0);
set D = digits (k,b);
set ND = (<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b));
A2: len <%1%> = 1 by AFINSQ_1:34;
n >= 1 + 0 by A1, NAT_1:13;
then ( len ((n -' 1) --> 0) = n -' 1 & n -' 1 = n - 1 ) by XREAL_1:233;
then A3: len (<%1%> ^ ((n -' 1) --> 0)) = 1 + (n - 1) by A2, AFINSQ_1:17;
then A4: len ((<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b))) = n + (len (digits (k,b))) by AFINSQ_1:17;
1 <= len (digits (k,b)) by A1, NUMERAL1:4;
then (len (<%1%> ^ ((n -' 1) --> 0))) + 1 <= len ((<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b))) by A3, A4, XREAL_1:6;
then A5: len (<%1%> ^ ((n -' 1) --> 0)) <= (len ((<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b)))) - 1 by XREAL_1:19;
(len ((<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b)))) - 1 < (len ((<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b)))) - 0 by XREAL_1:15;
then ((<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b))) . ((len ((<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b)))) - 1) = (digits (k,b)) . (((len ((<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b)))) - 1) - n) by A3, A5, AFINSQ_1:19
.= (digits (k,b)) . ((len (digits (k,b))) - 1) by A4 ;
then A6: ((<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b))) . ((len ((<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b)))) - 1) <> 0 by A1, NUMERAL1:def 2;
for i being Nat st i in dom ((<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b))) holds
((<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b))) . i < b

proof

let i be Nat; :: thesis: ( i in dom ((<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b))) implies ((<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b))) . i < b )
assume i in dom ((<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b))) ; :: thesis: ((<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b))) . i < b

per cases then ( i in dom (<%1%> ^ ((n -' 1) --> 0)) or ex m being Nat st
( m in dom (digits (k,b)) & i = n + m ) ) by A3, AFINSQ_1:20;

suppose A7: i in dom (<%1%> ^ ((n -' 1) --> 0)) ; :: thesis: ((<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b))) . i < b

per cases ( i in dom <%1%> or ex m being Nat st
( m in dom ((n -' 1) --> 0) & i = (len <%1%>) + m ) ) by A7, AFINSQ_1:20;

suppose A8: i in dom <%1%> ; :: thesis: ((<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b))) . i < b

then A9: (<%1%> ^ ((n -' 1) --> 0)) . i = <%1%> . i by AFINSQ_1:def 3;
i in Segm 1 by A8, AFINSQ_1:33;
then i = 0 by NAT_1:14, NAT_1:44;
hence ((<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b))) . i < b by A1, A7, AFINSQ_1:def 3, A9; :: thesis: verum

end;

suppose ex m being Nat st
( m in dom ((n -' 1) --> 0) & i = (len <%1%>) + m ) ; :: thesis: ((<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b))) . i < b

then consider m being Nat such that
A10: ( m in dom ((n -' 1) --> 0) & i = (len <%1%>) + m ) ;
0 = ((n -' 1) --> 0) . m
.= (<%1%> ^ ((n -' 1) --> 0)) . i by A10, AFINSQ_1:def 3 ;
hence ((<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b))) . i < b by A1, A7, AFINSQ_1:def 3; :: thesis: verum

end;

end;

end;

suppose ex m being Nat st
( m in dom (digits (k,b)) & i = n + m ) ; :: thesis: ((<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b))) . i < b

then consider m being Nat such that
A11: ( m in dom (digits (k,b)) & i = n + m ) ;
(digits (k,b)) . m < b by A11, A1, NUMERAL1:def 2;
hence ((<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b))) . i < b by A11, A3, AFINSQ_1:def 3; :: thesis: verum

end;

end;

end;

then digits ((value (((<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b))),b)),b) = (<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b)) by A1, A6, NUMBER11:5;
hence digits (((k * (b |^ n)) + 1),b) = (<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b)) by A1, Th13; :: thesis: verum