reconsider d = 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 = )
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 ; :: 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 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 ;
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
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
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 ;
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 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:
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 ;
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 ;
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
.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (d9 . (i + 1)) by
.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + ((d . (i + 1)) * (b |^ (i + 1))) by
.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((g . (i + 1)) mod b) * (b |^ (i + 1))) by
.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) mod b) * (b |^ (i + 1))) by
.= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) - (b * ((f . (i + 1)) div B))) * (b |^ (i + 1))) by
.= (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 ;
A27: 0 in Segm (m + 1) by NAT_1:44;
then d9 . 0 = (d . 0) * (b |^ 0) by
.= ((g . 0) mod b) * (b |^ 0) by
.= ((f . 0) mod b) * (b |^ 0) by
.= (n mod b) * 1 by
.= N - (B * (N div B)) by
.= 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 then s . ld = n - ((f . (m + 1)) * (b |^ (m + 1))) by
.= n by ;
then A29: n = Sum d9 by ;
m < l by ;
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 ; :: 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 ;
then A32: (g . m) div b = 0 by A16;
d . ((len d) - 1) = (g . m) mod b by
.= g . m by ;
hence d . ((len d) - 1) <> 0 by ; :: 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 ; :: thesis: verum
end;
assume n = 0 ; :: thesis: ex b1 being XFinSequence of NAT st b1 =
take d ; :: thesis:
thus d = ; :: thesis: verum