let b be Nat; :: thesis: ( b > 1 implies for s being NAT -valued XFinSequence st len s > 0 & ( for i being Nat st i in dom s holds
s . i < b ) holds
( (s . ((len s) - 1)) * (b |^ ((len s) -' 1)) <= value (s,b) & value (s,b) < b |^ (len s) ) )
assume A1: b > 1 ; :: thesis: for s being NAT -valued XFinSequence st len s > 0 & ( for i being Nat st i in dom s holds
s . i < b ) holds
( (s . ((len s) - 1)) * (b |^ ((len s) -' 1)) <= value (s,b) & value (s,b) < b |^ (len s) )
let s be NAT -valued XFinSequence; :: thesis: ( len s > 0 & ( for i being Nat st i in dom s holds
s . i < b ) implies ( (s . ((len s) - 1)) * (b |^ ((len s) -' 1)) <= value (s,b) & value (s,b) < b |^ (len s) ) )
assume A2: ( len s > 0 & ( for i being Nat st i in dom s holds
s . i < b ) ) ; :: thesis: ( (s . ((len s) - 1)) * (b |^ ((len s) -' 1)) <= value (s,b) & value (s,b) < b |^ (len s) )
consider v being XFinSequence of NAT such that
A3: ( dom v = dom s & ( for i being Nat st i in dom v holds
v . i = (s . i) * (b |^ i) ) & value (s,b) = Sum v ) by NUMERAL1:def 1;
set i = (len s) -' 1;
A4: len s >= 1 by A2, NAT_1:14;
then (len s) -' 1 < len v by A3, XREAL_1:237;
then A5: (len s) -' 1 in dom v by AFINSQ_1:86;
then A6: ( v . ((len s) -' 1) = (s . ((len s) -' 1)) * (b |^ ((len s) -' 1)) & value (s,b) = Sum v ) by A3;
len v > 0 by A2, A3;
then (s . ((len s) -' 1)) * (b |^ ((len s) -' 1)) <= value (s,b) by A5, A6, AFINSQ_2:61;
hence (s . ((len s) - 1)) * (b |^ ((len s) -' 1)) <= value (s,b) by A4, XREAL_1:233; :: thesis: value (s,b) < b |^ (len s)
set dz = (len s) --> (b -' 1);
consider dzv being XFinSequence of NAT such that
A7: ( dom dzv = dom ((len s) --> (b -' 1)) & ( for i being Nat st i in dom dzv holds
dzv . i = (((len s) --> (b -' 1)) . i) * (b |^ i) ) & value (((len s) --> (b -' 1)),b) = Sum dzv ) by NUMERAL1:def 1;
A8: len v = len dzv by A7, A3;

now :: thesis: for i being Nat st i in dom v holds
v . i <= dzv . i

let i be Nat; :: thesis: ( i in dom v implies v . i <= dzv . i )
assume A9: i in dom v ; :: thesis: v . i <= dzv . i
then A10: v . i = (s . i) * (b |^ i) by A3;
(b -' 1) + 1 = (b - 1) + 1 by A1, XREAL_1:233;
then s . i < (b -' 1) + 1 by A9, A3, A2;
then s . i <= b -' 1 by NAT_1:13;
then A11: s . i <= b - 1 by A1, XREAL_1:233;
dzv . i = (((len s) --> (b -' 1)) . i) * (b |^ i) by A8, A9, A7
.= (b -' 1) * (b |^ i) by FUNCOP_1:7, A9, A3
.= (b - 1) * (b |^ i) by A1, XREAL_1:233 ;
hence v . i <= dzv . i by A10, A11, XREAL_1:64; :: thesis: verum

end;

then Sum v <= Sum dzv by A8, AFINSQ_2:57;
then value (s,b) <= (b |^ (len s)) - 1 by A7, A1, Th7, A3;
then value (s,b) < ((b |^ (len s)) - 1) + 1 by NAT_1:13;
hence value (s,b) < b |^ (len s) ; :: thesis: verum