Proof of a determinantal integration formula

While reading about random matrices I encountered the following formula in a blog post by Terence Tao.

If \( K ( x,y) \) is such that

1. \( \int\! dx \ K(x,x) = \alpha \) 
2. \( \int\! dy \ K(x,y) K(y,z) = K(x,z) \)

then \begin{equation}\label{eq:20151118a} \int dx_{n+1} \det_{i,j \le n+1} \left( K(x_i , x_j ) \right) = (\alpha - n) \det_{i,j \le n} \left( K(x_i , x_j ) \right) \end{equation} For simplicity I have written \( \int \) instead of \( \int_{\mathbb{R}} \). This formula is used when calculating n-point functions in the Gaussian Unitary Ensemble (GUE). Tao gives a short proof of \eqref{eq:20151118a} based on induction and the Laplace expansion of determinants. In this post, I give a proof using integration over Grassmann variables. The reason I am interested in this alternative proof is that I want to compress the calculation of n-point functions in the GUE as much as possible.
The proof of \eqref{eq:20151118a} proceeds as follows. I express the determinant as a Gaussian integral over Grassmann variables \begin{equation*} \det_{i,j \le n+1} \left( K(x_i , x_j ) \right) = \int \left( \prod_{i=1} ^ {n+1} d\theta_i d\bar\theta_i \right) \exp \left( \sum_{i,j=1}^{n+1} \bar\theta_i K(x_i, x_j) \theta_j \right) \end{equation*} The LHS of \eqref{eq:20151118a} is \begin{equation*} \int dx_{n+1} \int \left( \prod_{i=1} ^ {n+1} d\theta_i d\bar\theta_i \right) \exp \left( \sum_{i,j=1}^{n} \bar\theta_i K(x_i, x_j) \theta_j + X \right) \end{equation*} with \begin{equation*} X = \sum_{i=1}^n \bar\theta_i K(x_i,x_{n+1}) \theta_{n+1} +\sum_{j=1}^n \bar\theta_{n+1} K(x_{n+1},x_j) \theta_j + \bar\theta_{n+1} K(x_{n+1}, x_{n+1} ) \theta_{n+1} \end{equation*} I now perform the integration over \( \theta_{n+1},\bar\theta_{n+1} \). I therefore expand the exponential \begin{equation*} e^X = \Big(1 + \sum_{i=1}^n \bar\theta_i K(x_i,x_{n+1}) \theta_{n+1} \Big) \Big( 1 + \sum_{j=1}^n \bar\theta_{n+1} K(x_{n+1},x_j) \theta_j \Big) \Big( 1 + \bar\theta_{n+1} K(x_{n+1}, x_{n+1} ) \theta_{n+1} \Big) \end{equation*} Integrating over \( \theta_{n+1},\bar\theta_{n+1} \) picks the coefficient of \( \bar\theta_{n+1}\theta_{n+1} \), this gives \begin{equation*} K(x_{n+1}, x_{n+1} ) - \sum_{i,j=1}^n \bar\theta_i K(x_i,x_{n+1}) K(x_{n+1},x_j) \theta_j \end{equation*} At this point I have \begin{equation*} LHS = \int dx_{n+1} \int \left( \prod_{i=1} ^ {n} d\theta_i d\bar\theta_i \right) \exp \left( \sum_{i,j=1}^{n} \bar\theta_i K(x_i, x_j) \theta_j \right) \left( K(x_{n+1}, x_{n+1} ) - \sum_{i,j=1}^n \bar\theta_i K(x_i,x_{n+1}) K(x_{n+1},x_j) \theta_j\right) \end{equation*} Integrating over \( x_{n+1} \) then gives \begin{equation*} LHS = \int \left( \prod_{i=1} ^ {n} d\theta_i d\bar\theta_i \right) \exp \left( \sum_{i,j=1}^{n} \bar\theta_i K(x_i, x_j) \theta_j \right) \left( \alpha - \sum_{i,j=1}^n \bar\theta_i K(x_i,x_j) \theta_j \right) \end{equation*} I elaborate a bit on the second term: \begin{align*} & \int \left( \prod_{i=1} ^ {n} d\theta_i d\bar\theta_i \right) \exp \left( \sum_{i,j=1}^{n} \bar\theta_i K(x_i, x_j) \theta_j \right) \left( \sum_{i,j=1}^n \bar\theta_i K(x_i,x_j) \theta_j \right)\\ & = \int \left( \prod_{i=1} ^ {n} d\theta_i d\bar\theta_i \right) \frac{1}{(n-1)!} \left( \sum_{i,j=1}^n \bar\theta_i K(x_i,x_j) \theta_j \right)^{n-1} \left( \sum_{i,j=1}^n \bar\theta_i K(x_i,x_j) \theta_j \right)\\ & = n \int \left( \prod_{i=1} ^ {n} d\theta_i d\bar\theta_i \right) \frac{1}{n!} \left( \sum_{i,j=1}^n \bar\theta_i K(x_i,x_j) \theta_j \right)^n\\ & = n \int \left( \prod_{i=1} ^ {n} d\theta_i d\bar\theta_i \right) \exp \left( \sum_{i,j=1}^{n} \bar\theta_i K(x_i, x_j) \theta_j \right) \end{align*} It follows that \begin{align*} LHS &= \int \left( \prod_{i=1} ^ {n} d\theta_i d\bar\theta_i \right) \exp \left( \sum_{i,j=1}^{n} \bar\theta_i K(x_i, x_j) \theta_j \right) \left( \alpha - n\right)\\ &= (\alpha - n) \det_{i,j \le n} \left( K(x_i , x_j ) \right) \end{align*}
Further reading

1. An introduction to integrating over Grassmann variables can be found in Path Integrals in Quantum Mechanics by Jean Zinn-Justin 
2. Details and many formulas about integrating over Grassmann variables can also be found in appendix A in this paper.