theorem Th8: :: NUMBER11:8

for b being Nat st b > 1 holds
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) )