1: \begin{proof}

2: As for Lemma~\ref{lem:rigorous_justification}, the proof just consists in checking that the regularity (i.e. the fact that the Fourier coefficients belongs to $\ell^1_\gamma$) of the solution $X$ and of the data $\left(c_j\right)_{1\leq j\leq 9}$ allows to rigorously backtrack the manipulations made to obtain $F$ from the eigenproblem~\eqref{eq:expanded_eigen}. 

3: \end{proof}

4: