take F = id V; :: thesis: F is with_eigenvalues
thus F is with_eigenvalues by Lm2; :: thesis: verum