reconsider N = n, B = b as Element of NAT by ORDINAL1:def 13;
thus ( n <> 0 implies ex d being XFinSequence of st
( value d,b = n & d . ((len d) - 1) <> 0 & ( for i being Nat st i in dom d holds
( 0 <= d . i & d . i < b ) ) ) ) :: thesis:

proof

assume A2: n <> 0 ; :: thesis:
deffunc H₁( Nat, Element of NAT ) -> Element of NAT = $2 div B;
consider f being Function of NAT ,NAT such that
A3: ( f . 0 = N & ( for i being Nat holds f . (i + 1) = H₁(i,f . i) ) ) from NAT_1:sch 12();
defpred S₁[ Nat] means f . $1 = 0 ;
defpred S₂[ Nat] means ex i being Element of NAT st f . i = $1;
A4: ex k being Nat st S₂[k] by A3;
A5: for k being Nat st k <> 0 & S₂[k] holds
ex l being Nat st
( l < k & S₂[l] )

proof

let k be Nat; :: thesis:
assume A6: ( k <> 0 & S₂[k] ) ; :: thesis:
then consider i being Element of NAT such that
A7: f . i = k ;
take l = k div b; :: thesis:
( k > 0 & b > 1 ) by A1, A6;
hence l < k by INT_1:83; :: thesis:
take i + 1 ; :: thesis:
thus f . (i + 1) = l by A3, A7; :: thesis:

end;

S₂[ 0 ] from NAT_1:sch 7(A4, A5);
then A8: ex l being Nat st S₁[l] ;
consider l being Nat such that
A9: ( S₁[l] & ( for i being Nat st S₁[i] holds
l <= i ) ) from NAT_1:sch 5(A8);
consider m being Nat such that
A10: m + 1 = l by A2, A3, A9, NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
m < l by A10, NAT_1:13;
then A11: f . m <> 0 by A9;
A12: S₁[l] by A9;

A13: now

let i be Nat; :: thesis:
assume l <= i ; :: thesis:
assume S₁[i] ; :: thesis:
then f . (i + 1) = 0 div b by A3;
hence S₁[i + 1] by NAT_2:4; :: thesis:

end;

A15: for i being Nat st l <= i holds
S₁[i] from NAT_1:sch 8(A12, A13);

A16: now

let i be Element of NAT ; :: thesis:
assume m < i ; :: thesis:
then l <= i by A10, NAT_1:13;
hence f . i = 0 by A15; :: thesis:

end;

dom f = NAT by FUNCT_2:def 1;
then m + 1 c= dom f by ORDINAL1:def 2;
then dom (f | (m + 1)) = m + 1 by RELAT_1:91;
then A17: f | (m + 1) is XFinSequence by ORDINAL1:def 7;
rng (f | (m + 1)) c= NAT ;
then reconsider g = f | (m + 1) as XFinSequence of by A17, RELAT_1:def 19;
defpred S₃[ Element of NAT , Element of NAT ] means $2 = (g . $1) mod b;
A18: for i being Element of NAT st i in m + 1 holds
ex x being Element of NAT st S₃[i,x] ;
consider d being XFinSequence of such that
A19: ( dom d = m + 1 & ( for i being Element of NAT st i in m + 1 holds
S₃[i,d . i] ) ) from STIRL2_1:sch 6(A18);
take d ; :: thesis:
deffunc H₂( Element of NAT ) -> Element of NAT = (d . $1) * (b |^ $1);
consider d' being XFinSequence such that
A20: ( len d' = len d & ( for i being Element of NAT st i in len d holds
d' . i = H₂(i) ) ) from AFINSQ_1:sch 2();
rng d' c= NAT

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in rng d' ; :: thesis:
then consider i being set such that
A21: ( i in dom d' & d' . i = a ) by FUNCT_1:def 5;
reconsider i = i as Element of NAT by A21;
a = H₂(i) by A20, A21;
hence a in NAT ; :: thesis:

end;

then reconsider d' = d' as XFinSequence of by RELAT_1:def 19;
A23: for i being Nat st i in dom d' holds
d' . i = (d . i) * (b |^ i) by A20;
A24: m < m + 1 by NAT_1:13;
g . m = f . m by AFINSQ_1:1, FUNCT_1:72;
then f . (m + 1) = (g . m) div b by A3;
then A25: (g . m) div b = 0 by A16, A24;
consider s being Function of NAT ,NAT such that
A27: ( s . 0 = d' . 0 & ( for i being Element of NAT st i + 1 < len d' holds
s . (i + 1) = addnat . (s . i),(d' . (i + 1)) ) & addnat "**" d' = s . ((len d') - 1) ) by A20, A19, STIRL2_1:def 3;
defpred S₄[ Element of NAT ] means ( $1 < len d' implies s . $1 = n - ((f . ($1 + 1)) * (b |^ ($1 + 1))) );
A28: 0 in m + 1 by NAT_1:45;
then d' . 0 = (d . 0 ) * (b |^ 0 ) by A19, A20
.= ((g . 0 ) mod b) * (b |^ 0 ) by A19, A28
.= ((f . 0 ) mod b) * (b |^ 0 ) by A28, FUNCT_1:72
.= (n mod b) * 1 by A3, NEWTON:9
.= N - (B * (N div B)) by A1, NEWTON:77
.= n - ((n div b) * (b |^ 1)) by NEWTON:10
.= n - ((f . (0 + 1)) * (b |^ (0 + 1))) by A3 ;
then A29: S₄[ 0 ] by A27;

A30: now

let i be Element of NAT ; :: thesis:
assume A31: S₄[i] ; :: thesis:

now

assume A32: i + 1 < len d' ; :: thesis:
then A33: i + 1 in dom d' by NAT_1:45;
thus s . (i + 1) = addnat . (s . i),(d' . (i + 1)) by A27, A32
.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (d' . (i + 1)) by A31, A32, BINOP_2:def 23, NAT_1:13
.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + ((d . (i + 1)) * (b |^ (i + 1))) by A20, A33
.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((g . (i + 1)) mod b) * (b |^ (i + 1))) by A19, A20, A33
.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) mod b) * (b |^ (i + 1))) by A19, A20, A33, FUNCT_1:72
.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) - (b * ((f . (i + 1)) div B))) * (b |^ (i + 1))) by A1, NEWTON:77
.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) - (b * (f . ((i + 1) + 1)))) * (b |^ (i + 1))) by A3
.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) * (b |^ (i + 1))) - ((f . ((i + 1) + 1)) * (b * (b |^ (i + 1)))))
.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) * (b |^ (i + 1))) - ((f . ((i + 1) + 1)) * (b |^ ((i + 1) + 1)))) by NEWTON:11
.= n - ((f . ((i + 1) + 1)) * (b |^ ((i + 1) + 1))) ; :: thesis:

end;

hence S₄[i + 1] ; :: thesis:

end;

A34: for i being Element of NAT holds S₄[i] from NAT_1:sch 1(A29, A30);
reconsider ld = (len d') - 1 as Element of NAT by A20, A19;
s . ld = n - ((f . (m + 1)) * (b |^ (m + 1))) by A20, A19, A34, XREAL_1:46
.= n by A9, A10 ;
then n = Sum d' by A27;
hence value d,b = n by A20, A23, Def1; :: thesis:
d . ((len d) - 1) = (g . m) mod b by A19, AFINSQ_1:1
.= g . m by A1, A25, NAT_2:14, NAT_D:24 ;
hence d . ((len d) - 1) <> 0 by A11, AFINSQ_1:1, FUNCT_1:72; :: thesis:
let i be Nat; :: thesis:
assume i in dom d ; :: thesis:
then d . i = (g . i) mod b by A19;
hence ( 0 <= d . i & d . i < b ) by A1, NAT_D:1; :: thesis:

end;

assume n = 0 ; :: thesis:
reconsider d = <%0 %> as XFinSequence of ;
take d ; :: thesis:
thus d = <%0 %> ; :: thesis: