let n, b be Nat; :: thesis: value (<%n%>,b) = n
A1: Sum <%n%> = n by AFINSQ_2:53;

now :: thesis: for i being Nat st i in dom <%n%> holds
<%n%> . i = (<%n%> . i) * (b |^ i)

let i be Nat; :: thesis: ( i in dom <%n%> implies <%n%> . i = (<%n%> . i) * (b |^ i) )
assume i in dom <%n%> ; :: thesis: <%n%> . i = (<%n%> . i) * (b |^ i)
then i in 1 by AFINSQ_1:def 4;
then i in {0} by CARD_1:49;
then A2: i = 0 by TARSKI:def 1;
thus <%n%> . i = (<%n%> . i) * 1
.= (<%n%> . i) * (b |^ i) by A2, NEWTON:4 ; :: thesis: verum

end;

hence value (<%n%>,b) = n by A1, NUMERAL1:def 1; :: thesis: verum