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