let n, b be Nat; :: thesis: ( n > 0 & b > 1 implies digits ((n * b),b) = <%0%> ^ (digits (n,b)) )
assume A1: ( n > 0 & b > 1 ) ; :: thesis: digits ((n * b),b) = <%0%> ^ (digits (n,b))
set d = digits (n,b);
reconsider d0 = <%0%> ^ (digits (n,b)) as XFinSequence of NAT ;
A2: len (digits (n,b)) >= 1 by A1, NUMERAL1:4;
then reconsider ld1 = (len (digits (n,b))) - 1 as Nat ;
A3: len (digits (n,b)) >= len <%0%> by A2, AFINSQ_1:34;
A4: len d0 = (len (digits (n,b))) + (len <%0%>) by AFINSQ_1:def 3
.= (len (digits (n,b))) + 1 by AFINSQ_1:def 4 ;
then A5: len (digits (n,b)) < len d0 by NAT_1:13;
value ((digits (n,b)),b) = n by A1, NUMERAL1:5;
then consider d9 being XFinSequence of NAT such that
A6: ( dom d9 = dom (digits (n,b)) & ( for i being Nat st i in dom d9 holds
d9 . i = ((digits (n,b)) . i) * (b |^ i) ) & n = Sum d9 ) by NUMERAL1:def 1;
deffunc H₁() -> Element of NAT = len d9;
deffunc H₂( Nat) -> set = b * (d9 . $1);
consider d1 being XFinSequence such that
A7: ( len d1 = H₁() & ( for n being Nat st n in H₁() holds
d1 . n = H₂(n) ) ) from AFINSQ_1:sch 2();
rng d1 c= NAT

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in rng d1 or o in NAT )
assume o in rng d1 ; :: thesis: o in NAT
then consider k being object such that
A8: ( k in dom d1 & d1 . k = o ) by FUNCT_1:def 3;
reconsider k = k as Nat by A8;
d1 . k = b * (d9 . k) by A8, A7;
hence o in NAT by A8, ORDINAL1:def 12; :: thesis: verum

end;

then reconsider d1 = d1 as XFinSequence of NAT by RELAT_1:def 19;
for o being object st o in dom d1 holds
d1 . o = b * (d9 . o) by A7;
then A9: Sum d1 = b * (Sum d9) by A7, NUMERAL2:18;
reconsider d10 = <%0%> ^ d1 as XFinSequence of NAT ;
A10: Sum d10 = (Sum <%0%>) + (Sum d1) by AFINSQ_2:55
.= 0 + (n * b) by AFINSQ_2:53, A6, A9
.= n * b ;
A11: dom d10 = (len <%0%>) + (len (digits (n,b))) by A6, A7, AFINSQ_1:17
.= dom d0 by AFINSQ_1:17 ;

now :: thesis: for i being Nat st i in dom d0 holds
d10 . i = (d0 . i) * (b |^ i)

let i be Nat; :: thesis: ( i in dom d0 implies d10 . b₁ = (d0 . b₁) * (b |^ b₁) )
assume i in dom d0 ; :: thesis: d10 . b₁ = (d0 . b₁) * (b |^ b₁)

per cases then ( i in dom <%0%> or ex k being Nat st
( k in dom (digits (n,b)) & i = (len <%0%>) + k ) ) by AFINSQ_1:20;

suppose A12: i in dom <%0%> ; :: thesis: d10 . b₁ = (d0 . b₁) * (b |^ b₁)

then i in 1 by AFINSQ_1:33;
then A13: i = 0 by CARD_1:49;
thus d10 . i = <%0%> . i by A12, AFINSQ_1:def 3
.= (d0 . i) * 1 by A12, AFINSQ_1:def 3
.= (d0 . i) * (b |^ i) by NEWTON:4, A13 ; :: thesis: verum

end;

suppose ex k being Nat st
( k in dom (digits (n,b)) & i = (len <%0%>) + k ) ; :: thesis: d10 . b₁ = (d0 . b₁) * (b |^ b₁)

then consider k being Nat such that
A14: ( k in dom (digits (n,b)) & i = (len <%0%>) + k ) ;
thus d10 . i = d1 . k by A14, AFINSQ_1:def 3, A6, A7
.= H₂(k) by A14, A6, A7
.= b * (((digits (n,b)) . k) * (b |^ k)) by A6, A14
.= ((digits (n,b)) . k) * (b * (b |^ k))
.= ((digits (n,b)) . k) * (b |^ (k + 1)) by NEWTON:6
.= ((digits (n,b)) . k) * (b |^ i) by A14, AFINSQ_1:34
.= (d0 . i) * (b |^ i) by A14, AFINSQ_1:def 3 ; :: thesis: verum

end;

end;

end;

then A15: value (d0,b) = n * b by A10, A11, NUMERAL1:def 1;
d0 . ((len d0) - 1) = (digits (n,b)) . ((len (digits (n,b))) - (len <%0%>)) by AFINSQ_1:19, A3, A5, A4
.= (digits (n,b)) . ld1 by AFINSQ_1:34 ;
then A16: d0 . ((len d0) - 1) <> 0 by A1, NUMERAL1:def 2;

now :: thesis: for i being Nat st i in dom d0 holds
( 0 <= d0 . i & d0 . i < b )

let i be Nat; :: thesis: ( i in dom d0 implies ( 0 <= d0 . b₁ & d0 . b₁ < b ) )
assume i in dom d0 ; :: thesis: ( 0 <= d0 . b₁ & d0 . b₁ < b )
then d0 . i in rng d0 by FUNCT_1:3;
then d0 . i in (rng <%0%>) \/ (rng (digits (n,b))) by AFINSQ_1:26;

per cases then ( d0 . i in rng <%0%> or d0 . i in rng (digits (n,b)) ) by XBOOLE_0:def 3;

suppose d0 . i in rng <%0%> ; :: thesis: ( 0 <= d0 . b₁ & d0 . b₁ < b )

then d0 . i in {0} by AFINSQ_1:33;
hence ( 0 <= d0 . i & d0 . i < b ) by A1; :: thesis: verum

end;

suppose d0 . i in rng (digits (n,b)) ; :: thesis: ( 0 <= d0 . b₁ & d0 . b₁ < b )

then consider o being object such that
A17: ( o in dom (digits (n,b)) & d0 . i = (digits (n,b)) . o ) by FUNCT_1:def 3;
thus ( 0 <= d0 . i & d0 . i < b ) by A17, A1, NUMERAL1:def 2; :: thesis: verum

end;

end;

end;

hence digits ((n * b),b) = <%0%> ^ (digits (n,b)) by A15, A16, A1, NUMERAL1:def 2; :: thesis: verum