David,
I should perhaps have mentioned that though your formulation of 9.1 is
correct, what you have for 9.2 does not capture that theorem correctly,
because your "sum n" adds the first n natural numbers, not the first n
elements of a sequence.
To get 9.2 you need to use the function "sigma" p
David,
Good to see you are making some progress.
For the examples in 9.2 you best course is probably to have a power
function with type:
ℝ→ℕ→ℝ
ⓈHOLCONST
│ pow:ℝ→ℕ→ℝ
├──
│ ∀b e⦁ (pow b 0) = 1. ∧
│ (pow b (e + 1)) = b * (pow b e)
■
This will fit with Rob's suggestion for modelling s
