let n, b be Nat; :: thesis: ( b > 1 implies n = (b * (value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b))) + ((digits (n,b)) . 0) )
assume A1: b > 1 ; :: thesis: n = (b * (value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b))) + ((digits (n,b)) . 0)
set d = digits (n,b);
A2: len (digits (n,b)) >= 1 by A1, NUMERAL1:4;
then A3: 0 in Segm (dom (digits (n,b))) by NAT_1:44;
n = value ((digits (n,b)),b) by A1, NUMERAL1:5;
then consider d1 being XFinSequence of NAT such that
A4: ( dom d1 = dom (digits (n,b)) & ( for i being Nat st i in dom d1 holds
d1 . i = ((digits (n,b)) . i) * (b |^ i) ) & n = Sum d1 ) by NUMERAL1:def 1;
d1 <> {} by A4, A2;
then d1 = <%(d1 . 0)%> ^ (d1 /^ 1) by Th2;
then A5: n = (Sum <%(d1 . 0)%>) + (Sum (d1 /^ 1)) by A4, AFINSQ_2:55
.= (d1 . 0) + (Sum (d1 /^ 1)) by AFINSQ_2:53
.= (Sum (d1 /^ 1)) + (((digits (n,b)) . 0) * (b |^ 0)) by A4, A3
.= (Sum (d1 /^ 1)) + (((digits (n,b)) . 0) * 1) by NEWTON:4 ;
consider e being XFinSequence of NAT such that
A6: ( dom e = dom ((digits (n,b)) /^ 1) & ( for i being Nat st i in dom e holds
e . i = (((digits (n,b)) /^ 1) . i) * (b |^ i) ) & value (((digits (n,b)) /^ 1),b) = Sum e ) by NUMERAL1:def 1;
A7: dom (d1 /^ 1) = len (d1 /^ 1)
.= (len d1) -' 1 by AFINSQ_2:def 2
.= (len (digits (n,b))) -' 1 by A4
.= len ((digits (n,b)) /^ 1) by AFINSQ_2:def 2
.= dom ((digits (n,b)) /^ 1) ;

now :: thesis: for n1 being object st n1 in dom e holds
(d1 /^ 1) . n1 = b * (e . n1)

let n1 be object ; :: thesis: ( n1 in dom e implies (d1 /^ 1) . n1 = b * (e . n1) )
assume A8: n1 in dom e ; :: thesis: (d1 /^ 1) . n1 = b * (e . n1)
then reconsider n = n1 as Nat ;
n in len ((digits (n,b)) /^ 1) by A6, A8;
then n in Segm ((len (digits (n,b))) -' 1) by AFINSQ_2:def 2;
then n + 1 < ((len (digits (n,b))) -' 1) + 1 by NAT_1:44, XREAL_1:8;
then n + 1 < len (digits (n,b)) by XREAL_1:235, A2;
then A9: n + 1 in Segm (dom (digits (n,b))) by NAT_1:44;
thus (d1 /^ 1) . n1 = d1 . (n + 1) by A7, A6, A8, AFINSQ_2:def 2
.= ((digits (n,b)) . (n + 1)) * (b |^ (n + 1)) by A4, A9
.= ((digits (n,b)) . (n + 1)) * ((b |^ n) * b) by NEWTON:6
.= b * (((digits (n,b)) . (n + 1)) * (b |^ n))
.= b * ((((digits (n,b)) /^ 1) . n) * (b |^ n)) by A8, A6, AFINSQ_2:def 2
.= b * (e . n1) by A8, A6 ; :: thesis: verum

end;

then Sum (d1 /^ 1) = b * (Sum e) by A7, A6, Th18;
hence n = (b * (value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b))) + ((digits (n,b)) . 0) by Th3, A6, A5; :: thesis: verum