let k, m, n be Nat; :: thesis: for b being Nat holds value (<%n,m,k%>,b) = ((k * (b |^ 2)) + (m * b)) + n
let b be Nat; :: thesis: value (<%n,m,k%>,b) = ((k * (b |^ 2)) + (m * b)) + n
reconsider f = <%n,m%> as 2 -element XFinSequence of NAT ;
<%n,m,k%> = f ^ <%k%> by AFINSQ_1:37;
then value (<%n,m,k%>,b) = (k * (b |^ 2)) + (value (<%n,m%>,b)) by VFN
.= (k * (b |^ 2)) + ((m * b) + n) by KBN ;
hence value (<%n,m,k%>,b) = ((k * (b |^ 2)) + (m * b)) + n ; :: thesis: verum