let b, n, k, x be Nat; :: thesis: ( b > 1 & n > 0 & n * (b |^ k) <= x & x < (n + 1) * (b |^ k) implies digits (n,b) = (digits (x,b)) /^ k )
assume that
A1: ( b > 1 & n > 0 ) and
A2: ( n * (b |^ k) <= x & x < (n + 1) * (b |^ k) ) ; :: thesis: digits (n,b) = (digits (x,b)) /^ k

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

suppose A3: k = 0 ; :: thesis: digits (n,b) = (digits (x,b)) /^ k

then ( n * 1 <= x & x < (n + 1) * 1 ) by A2, NEWTON:4;
then ( n <= x & x <= n ) by NAT_1:13;
then n = x by XXREAL_0:1;
hence digits (n,b) = (digits (x,b)) /^ k by A3, AFINSQ_2:10; :: thesis: verum

end;

suppose A4: k > 0 ; :: thesis: digits (n,b) = (digits (x,b)) /^ k

set D = digits (x,b);
set Dk = (digits (x,b)) | k;
set K = (digits (x,b)) /^ k;
A5: n * (b |^ k) >= 1 * (b |^ k) by A1, NAT_1:14, XREAL_1:64;
x < b |^ (len (digits (x,b))) by A1, NUMBER11:9;
then n * (b |^ k) < b |^ (len (digits (x,b))) by A2, XXREAL_0:2;
then b to_power k < b to_power (len (digits (x,b))) by A5, XXREAL_0:2;
then k < len (digits (x,b)) by A1, PRE_FF:8;
then A6: len ((digits (x,b)) | k) = k by AFINSQ_1:54;
A7: ((digits (x,b)) | k) ^ ((digits (x,b)) /^ k) = digits (x,b) ;
then A8: value ((digits (x,b)),b) = (value (((digits (x,b)) | k),b)) + ((value (((digits (x,b)) /^ k),b)) * (b |^ k)) by A6, Th1;
A9: x <> 0 by A1, A2;
for i being Nat st i in dom ((digits (x,b)) | k) holds
((digits (x,b)) | k) . i < b

proof

let i be Nat; :: thesis: ( i in dom ((digits (x,b)) | k) implies ((digits (x,b)) | k) . i < b )
assume A10: i in dom ((digits (x,b)) | k) ; :: thesis: ((digits (x,b)) | k) . i < b
dom ((digits (x,b)) | k) c= dom (digits (x,b)) by A7, AFINSQ_1:21;
then (digits (x,b)) . i < b by A10, A1, A9, NUMERAL1:def 2;
hence ((digits (x,b)) | k) . i < b by A7, A10, AFINSQ_1:def 3; :: thesis: verum

end;

then A11: ( 0 <= (value (((digits (x,b)) | k),b)) / (b |^ k) & (value (((digits (x,b)) | k),b)) / (b |^ k) < 1 ) by A6, A4, A1, NUMBER11:8, XREAL_1:191;
x <> 0 by A1, A2;
then x = (value (((digits (x,b)) | k),b)) + ((value (((digits (x,b)) /^ k),b)) * (b |^ k)) by A8, A1, NUMERAL1:def 2;
then A12: ( (n * (b |^ k)) / (b |^ k) <= ((value (((digits (x,b)) | k),b)) + ((value (((digits (x,b)) /^ k),b)) * (b |^ k))) / (b |^ k) & ((value (((digits (x,b)) | k),b)) + ((value (((digits (x,b)) /^ k),b)) * (b |^ k))) / (b |^ k) < ((n + 1) * (b |^ k)) / (b |^ k) ) by A1, A2, XREAL_1:72, XREAL_1:74;
((value (((digits (x,b)) | k),b)) + ((value (((digits (x,b)) /^ k),b)) * (b |^ k))) / (b |^ k) = ((value (((digits (x,b)) | k),b)) / (b |^ k)) + (((value (((digits (x,b)) /^ k),b)) * (b |^ k)) / (b |^ k)) by XCMPLX_1:62
.= ((value (((digits (x,b)) | k),b)) / (b |^ k)) + (value (((digits (x,b)) /^ k),b)) by A1, XCMPLX_1:89 ;
then A13: ( n <= ((value (((digits (x,b)) | k),b)) / (b |^ k)) + (value (((digits (x,b)) /^ k),b)) & ((value (((digits (x,b)) | k),b)) / (b |^ k)) + (value (((digits (x,b)) /^ k),b)) < n + 1 ) by A12, A1, XCMPLX_1:89;
then A14: ( n - ((value (((digits (x,b)) | k),b)) / (b |^ k)) <= (((value (((digits (x,b)) | k),b)) / (b |^ k)) + (value (((digits (x,b)) /^ k),b))) - ((value (((digits (x,b)) | k),b)) / (b |^ k)) & (((value (((digits (x,b)) | k),b)) / (b |^ k)) + (value (((digits (x,b)) /^ k),b))) - ((value (((digits (x,b)) | k),b)) / (b |^ k)) = value (((digits (x,b)) /^ k),b) ) by XREAL_1:9;
n - ((value (((digits (x,b)) | k),b)) / (b |^ k)) > n - 1 by A11, XREAL_1:15;
then n - 1 < value (((digits (x,b)) /^ k),b) by A14, XXREAL_0:2;
then A15: (n - 1) + 1 <= value (((digits (x,b)) /^ k),b) by INT_1:7;
A16: value (((digits (x,b)) /^ k),b) < (n + 1) - ((value (((digits (x,b)) | k),b)) / (b |^ k)) by A13, XREAL_1:20;
(n + 1) - ((value (((digits (x,b)) | k),b)) / (b |^ k)) <= (n + 1) - 0 by XREAL_1:13;
then value (((digits (x,b)) /^ k),b) < n + 1 by A16, XXREAL_0:2;
then value (((digits (x,b)) /^ k),b) <= n by NAT_1:13;
then A17: digits ((value (((digits (x,b)) /^ k),b)),b) = digits (n,b) by A15, XXREAL_0:1;
A18: (digits (x,b)) /^ k <> {} by A15, A1, NUMBER11:1;
then reconsider L = (len ((digits (x,b)) /^ k)) - 1 as Nat ;
A19: (len ((digits (x,b)) | k)) + (len ((digits (x,b)) /^ k)) = len (digits (x,b)) by A7, AFINSQ_1:17;
L < L + 1 by NAT_1:13;
then L in Segm (len ((digits (x,b)) /^ k)) by NAT_1:44;
then A20: (digits (x,b)) . (k + L) = ((digits (x,b)) /^ k) . L by A7, A6, AFINSQ_1:def 3;
A21: (digits (x,b)) . ((len (digits (x,b))) - 1) <> 0 by A9, A1, NUMERAL1:def 2;
for i being Nat st i in dom ((digits (x,b)) /^ k) holds
((digits (x,b)) /^ k) . i < b

proof

let i be Nat; :: thesis: ( i in dom ((digits (x,b)) /^ k) implies ((digits (x,b)) /^ k) . i < b )
assume A22: i in dom ((digits (x,b)) /^ k) ; :: thesis: ((digits (x,b)) /^ k) . i < b
i + k in dom (digits (x,b)) by A6, A7, A22, AFINSQ_1:23;
then (digits (x,b)) . (k + i) < b by A1, A9, NUMERAL1:def 2;
hence ((digits (x,b)) /^ k) . i < b by A7, A22, A6, AFINSQ_1:def 3; :: thesis: verum

end;

hence digits (n,b) = (digits (x,b)) /^ k by A17, A1, A18, A21, A19, A20, A6, NUMBER11:5; :: thesis: verum

end;

end;