let K be Field; :: thesis: for V being non trivial VectSp of K holds
( id V is with_eigenvalues & 1_ K is eigenvalue of id V & ( for v being Vector of V holds v is eigenvector of id V, 1_ K ) )
let V be non trivial VectSp of K; :: thesis: ( id V is with_eigenvalues & 1_ K is eigenvalue of id V & ( for v being Vector of V holds v is eigenvector of id V, 1_ K ) )
thus A1: id V is with_eigenvalues by Lm2; :: thesis: ( 1_ K is eigenvalue of id V & ( for v being Vector of V holds v is eigenvector of id V, 1_ K ) )
ex v being Vector of V st
( v <> 0. V & (id V) . v = (1_ K) * v ) by Lm2;
hence A2: 1_ K is eigenvalue of id V by A1, Def2; :: thesis: for v being Vector of V holds v is eigenvector of id V, 1_ K
let w be Vector of V; :: thesis: w is eigenvector of id V, 1_ K
(id V) . w = w
.= (1_ K) * w ;
hence w is eigenvector of id V, 1_ K by A1, A2, Def3; :: thesis: verum