theorem Th1: :: NUMBER16:1

for b being Nat
for f, g being XFinSequence of NAT holds value ((f ^ g),b) = (value (f,b)) + ((value (g,b)) * (b |^ (len f)))