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 :: thesis: for i being Nat st i in dom <%0%> holds
<%0%> . i = ((digits (n,b)) . i) * (b |^ i)

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 4, CARD_1:49;
then A4: i = 0 by TARSKI:def 1;
hence <%0%> . i = 0 * (b |^ i)
.= ((digits (n,b)) . i) * (b |^ i) by A3, A4 ;
:: 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:53; :: thesis: verum

end;

end;