let n, k, b be Nat; ( b > 1 & k > 0 implies value (((n --> (b -' 1)) ^ (digits ((k -' 1),b))),b) = (k * (b |^ n)) - 1 )
assume A1:
( b > 1 & k > 0 )
; value (((n --> (b -' 1)) ^ (digits ((k -' 1),b))),b) = (k * (b |^ n)) - 1
0 + 1 <= k
by A1, NAT_1:13;
then A2:
(k -' 1) + 1 = (k - 1) + 1
by XREAL_1:233;
len (n --> (b -' 1)) = n
;
hence value (((n --> (b -' 1)) ^ (digits ((k -' 1),b))),b) =
(value ((n --> (b -' 1)),b)) + ((value ((digits ((k -' 1),b)),b)) * (b |^ n))
by NUMBER16:1
.=
((b |^ n) - 1) + ((value ((digits ((k -' 1),b)),b)) * (b |^ n))
by A1, NUMBER11:7
.=
((b |^ n) - 1) + ((k -' 1) * (b |^ n))
by A1, NUMERAL1:5
.=
(k * (b |^ n)) - 1
by A2
;
verum