theorem Th16: :: NUMBER16:16

for n being Nat holds value ((<%1%> ^ (n --> 3)),10) = ((10 |^ (n + 1)) - 7) / 3