let b be Nat; :: thesis: ( b > 1 implies 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 )
assume A1: b > 1 ; :: thesis: 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
let s be NAT -valued XFinSequence; :: thesis: ( len s > 0 & s . ((len s) - 1) <> 0 & ( for i being Nat st i in dom s holds
s . i < b ) implies digits ((value (s,b)),b) = s )
assume A2: ( len s > 0 & s . ((len s) - 1) <> 0 & ( for i being Nat st i in dom s holds
s . i < b ) ) ; :: thesis: digits ((value (s,b)),b) = s
reconsider l = (len s) - 1 as Nat by A2, NAT_1:20;
A3: b |^ l <> 0 by A1;
consider d9 being XFinSequence of NAT such that
A4: ( dom d9 = dom s & ( for i being Nat st i in dom d9 holds
d9 . i = (s . i) * (b |^ i) ) & value (s,b) = Sum d9 ) by NUMERAL1:def 1;
A5: len d9 <> 0 by A2, A4;
l in dom d9 by A2, A4, FUNCT_1:def 2;
then d9 . l = (s . l) * (b |^ l) by A4;
then d9 . l <> 0 by A2, A3, XCMPLX_1:6;
then ((len d9) --> 0) . l <> d9 . l ;
then A6: value (s,b) <> 0 by A4, AFINSQ_2:62, A5;
for i being Nat st i in dom s holds
( s . i >= 0 & s . i < b ) by A2;
hence digits ((value (s,b)),b) = s by A6, A1, A2, NUMERAL1:def 2; :: thesis: verum