theorem Th5: :: NUMBER11:5

for b being Nat st b > 1 holds
for s being NAT -valued XFinSequence st len s > 0 & s . ((len s) - 1) <> 0 & ( for i being Nat st i in dom s holds
s . i < b ) holds
digits ((value (s,b)),b) = s