let n, k, b be Nat; :: thesis: ( b > 1 & k > 0 & n > 0 implies value (((<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b))),b) = (k * (b |^ n)) + 1 )
assume A1: ( b > 1 & k > 0 & n > 0 ) ; :: thesis: value (((<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b))),b) = (k * (b |^ n)) + 1
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;
value ((<%1%> ^ ((n -' 1) --> 0)),b) = (value (<%1%>,b)) + ((value (((n -' 1) --> 0),b)) * (b |^ 1)) by A2, NUMBER16:1
.= (value (<%1%>,b)) + (0 * (b |^ 1)) by Th12
.= 1 by NUMBER11:2 ;
hence value (((<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b))),b) = 1 + ((value ((digits (k,b)),b)) * (b |^ n)) by A3, NUMBER16:1
.= (k * (b |^ n)) + 1 by A1, NUMERAL1:5 ;
:: thesis: verum