let n, b be Nat; :: thesis: ( b > 1 implies value (digits n,b),b = n )
assume A1: b > 1 ; :: thesis: value (digits n,b),b = n

per cases ( n <> 0 or n = 0 ) ;

suppose n <> 0 ; :: thesis: value (digits n,b),b = n

hence value (digits n,b),b = n by A1, Def2; :: thesis: verum

end;

suppose A2: n = 0 ; :: thesis: value (digits n,b),b = n

then A3: digits n,b = <%0 %> by A1, Def2;

now

let i be Nat; :: thesis: ( i in dom <%0 %> implies <%0 %> . i = ((digits n,b) . i) * (b |^ i) )
assume i in dom <%0 %> ; :: thesis: <%0 %> . i = ((digits n,b) . i) * (b |^ i)
then i in {0 } by AFINSQ_1:def 5, CARD_1:87;
then A4: i = 0 by TARSKI:def 1;
hence <%0 %> . i = 0 * (b |^ i) by AFINSQ_1:def 5
.= ((digits n,b) . i) * (b |^ i) by A3, A4, AFINSQ_1:def 5 ;
:: thesis: verum

end;

then value (digits n,b),b = Sum <%0 %> by A3, Def1;
hence value (digits n,b),b = n by A2, AFINSQ_2:65; :: thesis: verum

end;

end;