let K be Field; :: thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1 st not ker f is trivial holds
( f is with_eigenvalues & 0. K is eigenvalue of f )
let V1 be VectSp of K; :: thesis: for f being linear-transformation of V1,V1 st not ker f is trivial holds
( f is with_eigenvalues & 0. K is eigenvalue of f )
let f be linear-transformation of V1,V1; :: thesis: ( not ker f is trivial implies ( f is with_eigenvalues & 0. K is eigenvalue of f ) )
assume A1: not ker f is trivial ; :: thesis: ( f is with_eigenvalues & 0. K is eigenvalue of f )
consider v being Vector of (ker f) such that
A2: v <> 0. (ker f) by A1, STRUCT_0:def 19;
reconsider v = v as Vector of V1 by VECTSP_4:18;
A3: v <> 0. V1 by A2, VECTSP_4:19;
A4: f . v = 0. V1 by RANKNULL:14
.= (0. K) * v by VECTSP_1:59 ;
then f is with_eigenvalues by A3, Def1;
hence ( f is with_eigenvalues & 0. K is eigenvalue of f ) by A3, A4, Def2; :: thesis: verum