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 ) )
consider v being Vector of V such that
A2: ( v <> 0. V & (id V) . v = (1_ K) * v ) by Lm2;
thus A3: 1_ K is eigenvalue of id V by A1, A2, 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 by FUNCT_1:34
.= (1_ K) * w by VECTSP_1:def 26 ;
hence w is eigenvector of id V, 1_ K by A1, A3, Def3; :: thesis: verum