reconsider d = <%0%> as XFinSequence of NAT ;
reconsider N = n, B = b as Element of NAT by ORDINAL1:def 12;
thus ( n <> 0 implies ex d being XFinSequence of NAT 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: ( not n <> 0 implies ex b1 being XFinSequence of NAT st b1 = <%0%> )
proof
deffunc H1( Nat, Element of NAT ) -> Element of NAT = $2 div B;
consider f being sequence of NAT such that
A2: ( f . 0 = N & ( for i being Nat holds f . (i + 1) = H1(i,f . i) ) ) from NAT_1:sch 12();
 defpred S1[ Nat] means f . $1 = 0 ;
defpred S2[ Nat] means ex i being Nat st f . i = $1;
A3: for k being Nat st k <> 0 & S2[k] holds
ex l being Nat st
( l < k & S2[l] )
proof
let k be Nat; :: thesis: ( k <> 0 & S2[k] implies ex l being Nat st
( l < k & S2[l] ) )
assume that
A4: k <> 0 and
A5: S2[k] ; :: thesis: ex l being Nat st
( l < k & S2[l] )
take l = k div b; :: thesis: ( l < k & S2[l] )
thus l < k by A1, A4, INT_1:56; :: thesis: S2[l]
consider i being Nat such that
A6: f . i = k by A5;
take i + 1 ; :: thesis: f . (i + 1) = l
thus f . (i + 1) = l by A2, A6; :: thesis: verum
end;
A7: ex k being Nat st S2[k] by A2;
S2[ 0 ] from NAT_1:sch 7(A7, A3);
 then A8: ex l being Nat st S1[l] ;
consider l being Nat such that
A9: ( S1[l] & ( for i being Nat st S1[i] holds
l <= i ) ) from NAT_1:sch 5(A8);
 assume n <> 0 ; :: thesis: ex d being XFinSequence of NAT 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 ) ) )
then consider m being Nat such that
A10: m + 1 = l by A2, A9, NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
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:62;
then reconsider g = f | (m + 1) as XFinSequence of NAT by ORDINAL1:def 7;
defpred S3[ Nat, Nat] means $2 = (g . $1) mod b;
A11: for i being Nat st i in Segm (m + 1) holds
ex x being Element of NAT st S3[i,x] ;
consider d being XFinSequence of NAT such that
A12: ( dom d = Segm (m + 1) & ( for i being Nat st i in Segm (m + 1) holds
S3[i,d . i] ) ) from STIRL2_1:sch 5(A11);
A13: now :: thesis: for i being Nat st l <= i & S1[i] holds
S1[i + 1]
let i be Nat; :: thesis: ( l <= i & S1[i] implies S1[i + 1] )
assume l <= i ; :: thesis: ( S1[i] implies S1[i + 1] )
assume S1[i] ; :: thesis: S1[i + 1]
then f . (i + 1) = 0 div b by A2;
hence S1[i + 1] by NAT_2:2; :: thesis: verum
end;
A14: S1[l] by A9;
A15: for i being Nat st l <= i holds
S1[i] from NAT_1:sch 8(A14, A13);
A16: now :: thesis: for i being Element of NAT st m < i holds
f . i = 0
let i be Element of NAT ; :: thesis: ( m < i implies f . i = 0 )
assume m < i ; :: thesis: f . i = 0
then l <= i by A10, NAT_1:13;
hence f . i = 0 by A15; :: thesis: verum
end;
deffunc H2( Nat) -> set = (d . $1) * (b |^ $1);
consider d9 being XFinSequence such that
A17: ( len d9 = len d & ( for i being Nat st i in len d holds
d9 . i = H2(i) ) ) from AFINSQ_1:sch 2();
 rng d9 c= NAT
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng d9 or a in NAT )
assume a in rng d9 ; :: thesis: a in NAT
then consider i being object such that
A18: i in dom d9 and
A19: d9 . i = a by FUNCT_1:def 3;
reconsider i = i as Element of NAT by A18;
a = H2(i) by A17, A18, A19;
hence a in NAT by ORDINAL1:def 12; :: thesis: verum
end;
then reconsider d9 = d9 as XFinSequence of NAT by RELAT_1:def 19;
consider s being sequence of NAT such that
A20: s . 0 = d9 . 0 and
A21: for i being Nat st i + 1 < len d9 holds
s . (i + 1) = addnat . ((s . i),(d9 . (i + 1))) and
A22: addnat "**" d9 = s . ((len d9) - 1) by A12, A17, AFINSQ_2:def 8;
defpred S4[ Nat] means ( $1 < len d9 implies s . $1 = n - ((f . ($1 + 1)) * (b |^ ($1 + 1))) );
A23: now :: thesis: for i being Nat st S4[i] holds
S4[i + 1]
let i be Nat; :: thesis: ( S4[i] implies S4[i + 1] )
assume A24: S4[i] ; :: thesis: S4[i + 1]
now :: thesis: ( i + 1 < len d9 implies s . (i + 1) = n - ((f . ((i + 1) + 1)) * (b |^ ((i + 1) + 1))) )
assume A25: i + 1 < len d9 ; :: thesis: s . (i + 1) = n - ((f . ((i + 1) + 1)) * (b |^ ((i + 1) + 1)))
then A26: i + 1 in dom d9 by AFINSQ_1:86;
thus s . (i + 1) = addnat . ((s . i),(d9 . (i + 1))) by A21, A25
.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (d9 . (i + 1)) by A24, A25, BINOP_2:def 23, NAT_1:13
.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + ((d . (i + 1)) * (b |^ (i + 1))) by A17, A26
.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((g . (i + 1)) mod b) * (b |^ (i + 1))) by A12, A17, A26
.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) mod b) * (b |^ (i + 1))) by A12, A17, A26, FUNCT_1:49
.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) - (b * ((f . (i + 1)) div B))) * (b |^ (i + 1))) by A1, NEWTON:63
.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) - (b * (f . ((i + 1) + 1)))) * (b |^ (i + 1))) by A2
.= (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:6
.= n - ((f . ((i + 1) + 1)) * (b |^ ((i + 1) + 1))) ; :: thesis: verum
end;
hence S4[i + 1] ; :: thesis: verum
end;
reconsider ld = (len d9) - 1 as Element of NAT by A12, A17;
A27: 0 in Segm (m + 1) by NAT_1:44;
then d9 . 0 = (d . 0) * (b |^ 0) by A12, A17
.= ((g . 0) mod b) * (b |^ 0) by A12, A27
.= ((f . 0) mod b) * (b |^ 0) by A27, FUNCT_1:49
.= (n mod b) * 1 by A2, NEWTON:4
.= N - (B * (N div B)) by A1, NEWTON:63
.= n - ((n div b) * (b |^ 1))
.= n - ((f . (0 + 1)) * (b |^ (0 + 1))) by A2 ;
then A28: S4[ 0 ] by A20;
for i being Nat holds S4[i] from NAT_1:sch 2(A28, A23);
 then s . ld = n - ((f . (m + 1)) * (b |^ (m + 1))) by A12, A17, XREAL_1:44
.= n by A9, A10 ;
then A29: n = Sum d9 by A22, AFINSQ_2:51;
m < l by A10, NAT_1:13;
then A30: f . m <> 0 by A9;
take d ; :: thesis: ( 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 ) ) )
thus value (d,b) = n by A17, A29, Def1; :: thesis: ( d . ((len d) - 1) <> 0 & ( for i being Nat st i in dom d holds
( 0 <= d . i & d . i < b ) ) )
m in Segm (m + 1) by NAT_1:45;
then A31: g . m = f . m by FUNCT_1:49;
then ( m < m + 1 & f . (m + 1) = (g . m) div b ) by A2, NAT_1:13;
then A32: (g . m) div b = 0 by A16;
d . ((len d) - 1) = (g . m) mod b by A12, NAT_1:45
.= g . m by A1, A32, NAT_2:12, NAT_D:24 ;
hence d . ((len d) - 1) <> 0 by A30, A31; :: thesis: for i being Nat st i in dom d holds
( 0 <= d . i & d . i < b )
let i be Nat; :: thesis: ( i in dom d implies ( 0 <= d . i & d . i < b ) )
assume i in dom d ; :: thesis: ( 0 <= d . i & d . i < b )
then d . i = (g . i) mod b by A12;
hence ( 0 <= d . i & d . i < b ) by A1, NAT_D:1; :: thesis: verum
end;
assume n = 0 ; :: thesis: ex b1 being XFinSequence of NAT st b1 = <%0%>
take d ; :: thesis: d = <%0%>
thus d = <%0%> ; :: thesis: verum