let K be Field; :: thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K holds
( ( f is with_eigenvalues & L is eigenvalue of f ) iff not ker (f + ((- L) * (id V1))) is trivial )
let V1 be VectSp of K; :: thesis: for f being linear-transformation of V1,V1
for L being Scalar of K holds
( ( f is with_eigenvalues & L is eigenvalue of f ) iff not ker (f + ((- L) * (id V1))) is trivial )
let f be linear-transformation of V1,V1; :: thesis: for L being Scalar of K holds
( ( f is with_eigenvalues & L is eigenvalue of f ) iff not ker (f + ((- L) * (id V1))) is trivial )
let L be Scalar of K; :: thesis: ( ( f is with_eigenvalues & L is eigenvalue of f ) iff not ker (f + ((- L) * (id V1))) is trivial )

hereby :: thesis: ( not ker (f + ((- L) * (id V1))) is trivial implies ( f is with_eigenvalues & L is eigenvalue of f ) )

assume ( f is with_eigenvalues & L is eigenvalue of f ) ; :: thesis: not ker (f + ((- L) * (id V1))) is trivial
then consider v1 being Vector of V1 such that
A1: v1 <> 0. V1 and
A2: f . v1 = L * v1 by Def2;
(f + ((- L) * (id V1))) . v1 = (f . v1) + (((- L) * (id V1)) . v1) by MATRLIN:def 3
.= (f . v1) + ((- L) * ((id V1) . v1)) by MATRLIN:def 4
.= (f . v1) + ((- L) * v1)
.= (L + (- L)) * v1 by A2, VECTSP_1:def 15
.= (0. K) * v1 by VECTSP_1:19
.= 0. V1 by VECTSP_1:15 ;
then v1 in ker (f + ((- L) * (id V1))) by RANKNULL:10;
then A3: v1 is Element of (ker (f + ((- L) * (id V1)))) ;
v1 <> 0. (ker (f + ((- L) * (id V1)))) by A1, VECTSP_4:11;
hence not ker (f + ((- L) * (id V1))) is trivial by A3; :: thesis: verum

end;

assume not ker (f + ((- L) * (id V1))) is trivial ; :: thesis: ( f is with_eigenvalues & L is eigenvalue of f )
then consider v being Vector of (ker (f + ((- L) * (id V1)))) such that
A4: v <> 0. (ker (f + ((- L) * (id V1)))) ;
A5: v in ker (f + ((- L) * (id V1))) ;
reconsider v = v as Vector of V1 by VECTSP_4:10;
0. V1 = (f + ((- L) * (id V1))) . v by A5, RANKNULL:10
.= (f . v) + (((- L) * (id V1)) . v) by MATRLIN:def 3
.= (f . v) + ((- L) * ((id V1) . v)) by MATRLIN:def 4
.= (f . v) + ((- L) * v) ;
then A6: f . v = - ((- L) * v) by VECTSP_1:16
.= (- (- L)) * v by VECTSP_1:21
.= L * v by RLVECT_1:17 ;
A7: v <> 0. V1 by A4, VECTSP_4:11;
then f is with_eigenvalues by A6;
hence ( f is with_eigenvalues & L is eigenvalue of f ) by A6, A7, Def2; :: thesis: verum