let n, b be Nat; ( b > 1 implies n = (b * (value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b))) + ((digits (n,b)) . 0) )
assume A1:
b > 1
; 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 for n1 being object st n1 in dom e holds
(d1 /^ 1) . n1 = b * (e . n1)let n1 be
object ;
( n1 in dom e implies (d1 /^ 1) . n1 = b * (e . n1) )assume A8:
n1 in dom e
;
(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
;
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; verum