Spivak, Ch. 12 "Inverse Functions", Prob. 12: If $f'(f^{-1}(x)) \neq 0$ and $f^{(k)}(f^{-1}(x))$ exists, then $(f^{-1})^{(k)}(x)$ exists.

Question

Consider the following problem from chapter 12, "Inverse Functions", of Spivak's Calculus

12. Prove that if $f'(f^{-1}(x)) \neq 0$ and $f^{(k)}(f^{-1}(x))$ exists, then $(f^{-1})^{(k)}(x)$ exists.

The solution manual has the following solution

As in problems 10-21 and 10-33, the main difficulty is in formulating a reasonable conjecture for the form of $(f^{-1})^{(k)}(x)$. It is not hard to prove the following assertion by induction on $k$: If $f^{(k)}(f^{-1}(x))$ exists, and $f'(f^{-1}(x))$ is non-zero, then

$$(f^{-1})^{(k)}(x)=\frac{A(x)}{[f'(f^{-1}(x))]^m}$$

for some integer $m$, where $A(x)$ is the sum of terms of the form

$$[f'(f^{-1}(x)]^{m_1} \cdot ... \cdot [f^{(l)}(f^{-1}(x)]^{m_l}$$

Here is my attempt at filling in the steps in this proof

Consider the statement

$$\begin{array}{l} f^{(k)}(f^{-1}(x)) \text{ exists }\\ f'(f^{-1}(x)) \neq 0 \end{array} \implies (f^{-1})^{(k)}(x)=\frac{A(x)}{[f'(f^{-1}(x))]^m}\tag{1}$$

for some integer $m$, where $A(x)$ is the sum of terms of the form

$$[f'(f^{-1}(x)]^{m_1} \cdot ... \cdot [f^{(l)}(f^{-1}(x)]^{m_l}\tag{2}$$

1. where do $l$, and $m_1,m_2, ...m_l$ come from?
2. does the assumption that $f^{(k)}(f^{-1}(x))$ exists (for all $x$) imply that $f^{(k)}(y)$ exists for all $y$? Since $x=f^{-1}(y)$ for some $y$ in $f$'s domain, it would seem that the assumption is true for $f$'s entire domain.

I'm not sure where $l$ comes from, but $A(x)$ is a product of derivatives of $f$ of order $1$ to $l$, where I am guessing maybe $l\leq k$.

Proof

We use induction on $k$.

Let $k=1$. Then by assumption $f'(f^{-1}(x))$ exists and is $\neq 0$. Then by the inverse function theorem

$(f^{-1}(x))'$ exists and equals $\frac{1}{f'(f^{-1}(x)}$. Here $A(x)=1$, which means $m_1=m_2=...=m_l=0$.

Now assume the statement holds for some $k$.

Assume $f'(f^{-1}(x))$ exists and is $\neq 0$ and $f^{(k+1)}(f^{-1}(x))$ exists.

Then $f^{(k)}(f^{-1}(x))$ exists and by the inductive hypothesis equals $\frac{A(x)}{[f'(f^{-1}(x))]^m}$, where $l\leq k$.

Let $h(x)=f^{(k)}(f^{-1}(x))$. Then

$$h'(x)=\frac{d[f^{(k)}(f^{-1}(x))]}{dx}=f^{(k+1)}(f^{-1}(x))(f^{-1})'(x)$$

3. I am struggling to be certain that I can actually justify the Chain Rule above. $f^{(k)}(f^{-1}(x))$ is differentiable (everywhere if the answer to question $2$ above is yes) since $f^{(k+1)}(f^{-1}(x))$ exists by assumption, and $f^{-1}(x)$ is differentiable (everywhere) by the result of the base case. Hence we can apply the Chain Rule to $h(x)$. Is this correct?

But $x=f^{-1}(y)$, so $(f^{-1})'(x) \neq 0$. Therefore

$$f^{(k+1)}(f^{-1}(x))=\frac{\frac{d[f^{(k)}(f^{-1}(x))]}{dx}}{(f^{-1})'(x)}\tag{3}$$

$f^{(k+1)}(f^{-1}(x))$ exists. But does it have the form $(2)$?

4. Are the steps correct so far, and if so, is it the case that we must show that the numerator in $(3)$ has form $A(x)$?