let k, n, b be Nat; :: thesis: value (<%n,k%>,b) = (k * b) + n
consider x being XFinSequence of NAT such that
A2: ( dom x = dom <%n,k%> & ( for i being Nat st i in dom x holds
x . i = (<%n,k%> . i) * (b |^ i) ) & value (<%n,k%>,b) = Sum x ) by NUMERAL1:def 1;
A3: ( dom x = 2 & dom <%n,k%> = 2 & <%n,k%> . 0 = n & <%n,k%> . 1 = k ) by A2, AFINSQ_1:38;
A4: dom x = {0,1} by A2, AFINSQ_1:38, CARD_1:50;
A5: x . 0 = n * (1 * (b |^ 0))

proof

0 in dom x by A4, TARSKI:def 2;
then x . 0 = (<%n,k%> . 0) * (b |^ 0) by A2;
hence x . 0 = n * (1 * (b |^ 0)) ; :: thesis: verum

end;

x . 1 = k * (b |^ 1)

proof

1 in dom x by A4, TARSKI:def 2;
then x . 1 = (<%n,k%> . 1) * (b |^ 1) by A2;
hence x . 1 = k * (b |^ 1) ; :: thesis: verum

end;

then x = <%n,(k * b)%> by A3, A5, AFINSQ_1:38;
hence value (<%n,k%>,b) = (k * b) + n by A2, AFINSQ_2:54; :: thesis: verum