theorem :: NUMERAL3:72

for k, m, n, b being Nat holds value (<%n,m,k%>,b) = ((k * (b |^ 2)) + (m * b)) + n