let K be Field; :: thesis: for V1 being VectSp of K
for v1 being Vector of V1
for f being linear-transformation of V1,V1
for L being Scalar of K st f is with_eigenvalues & L is eigenvalue of f holds
( v1 is eigenvector of f,L iff v1 in ker (f + ((- L) * (id V1))) )
let V1 be VectSp of K; :: thesis: for v1 being Vector of V1
for f being linear-transformation of V1,V1
for L being Scalar of K st f is with_eigenvalues & L is eigenvalue of f holds
( v1 is eigenvector of f,L iff v1 in ker (f + ((- L) * (id V1))) )
let v1 be Vector of V1; :: thesis: for f being linear-transformation of V1,V1
for L being Scalar of K st f is with_eigenvalues & L is eigenvalue of f holds
( v1 is eigenvector of f,L iff v1 in ker (f + ((- L) * (id V1))) )
let f be linear-transformation of V1,V1; :: thesis: for L being Scalar of K st f is with_eigenvalues & L is eigenvalue of f holds
( v1 is eigenvector of f,L iff v1 in ker (f + ((- L) * (id V1))) )
let L be Scalar of K; :: thesis: ( f is with_eigenvalues & L is eigenvalue of f implies ( v1 is eigenvector of f,L iff v1 in ker (f + ((- L) * (id V1))) ) )
assume A1: ( f is with_eigenvalues & L is eigenvalue of f ) ; :: thesis: ( v1 is eigenvector of f,L iff v1 in ker (f + ((- L) * (id V1))) )

hereby :: thesis: ( v1 in ker (f + ((- L) * (id V1))) implies v1 is eigenvector of f,L )

assume v1 is eigenvector of f,L ; :: thesis: v1 in ker (f + ((- L) * (id V1)))
then A2: f . v1 = L * v1 by A1, Def3;
(f + ((- L) * (id V1))) . v1 = (f . v1) + (((- L) * (id V1)) . v1) by MATRLIN:def 5
.= (f . v1) + ((- L) * ((id V1) . v1)) by MATRLIN:def 6
.= (f . v1) + ((- L) * v1) by FUNCT_1:34
.= (L + (- L)) * v1 by A2, VECTSP_1:def 27
.= (0. K) * v1 by VECTSP_1:66
.= 0. V1 by VECTSP_1:60 ;
hence v1 in ker (f + ((- L) * (id V1))) by RANKNULL:10; :: thesis: verum

end;

assume v1 in ker (f + ((- L) * (id V1))) ; :: thesis: v1 is eigenvector of f,L
then 0. V1 = (f + ((- L) * (id V1))) . v1 by RANKNULL:10
.= (f . v1) + (((- L) * (id V1)) . v1) by MATRLIN:def 5
.= (f . v1) + ((- L) * ((id V1) . v1)) by MATRLIN:def 6
.= (f . v1) + ((- L) * v1) by FUNCT_1:34 ;
then f . v1 = - ((- L) * v1) by VECTSP_1:63
.= (- (- L)) * v1 by VECTSP_1:68
.= L * v1 by RLVECT_1:30 ;
hence v1 is eigenvector of f,L by A1, Def3; :: thesis: verum