theorem :: NUMERAL3:71

for k, n, b being Nat holds value (((k --> 0) ^ <%n%>),b) = n * (b |^ k)