let K be Field; :: thesis: for L being Scalar of K
for V1 being finite-dimensional VectSp of K
for b1, b1' being OrdBasis of V1
for f being linear-transformation of V1,V1 holds
( ( f is with_eigenvalues & L is eigenvalue of f ) iff Det (AutEqMt (f + ((- L) * (id V1))),b1,b1') = 0. K )
let L be Scalar of K; :: thesis: for V1 being finite-dimensional VectSp of K
for b1, b1' being OrdBasis of V1
for f being linear-transformation of V1,V1 holds
( ( f is with_eigenvalues & L is eigenvalue of f ) iff Det (AutEqMt (f + ((- L) * (id V1))),b1,b1') = 0. K )
let V1 be finite-dimensional VectSp of K; :: thesis: for b1, b1' being OrdBasis of V1
for f being linear-transformation of V1,V1 holds
( ( f is with_eigenvalues & L is eigenvalue of f ) iff Det (AutEqMt (f + ((- L) * (id V1))),b1,b1') = 0. K )
let b1, b1' be OrdBasis of V1; :: thesis: for f being linear-transformation of V1,V1 holds
( ( f is with_eigenvalues & L is eigenvalue of f ) iff Det (AutEqMt (f + ((- L) * (id V1))),b1,b1') = 0. K )
let f be linear-transformation of V1,V1; :: thesis: ( ( f is with_eigenvalues & L is eigenvalue of f ) iff Det (AutEqMt (f + ((- L) * (id V1))),b1,b1') = 0. K )
A1: dim V1 = dim V1 ;

hereby :: thesis: ( Det (AutEqMt (f + ((- L) * (id V1))),b1,b1') = 0. K implies ( f is with_eigenvalues & L is eigenvalue of f ) )

assume ( f is with_eigenvalues & L is eigenvalue of f ) ; :: thesis: Det (AutEqMt (f + ((- L) * (id V1))),b1,b1') = 0. K
then not ker (f + ((- L) * (id V1))) is trivial by Th14;
hence Det (AutEqMt (f + ((- L) * (id V1))),b1,b1') = 0. K by A1, MATRLIN2:50; :: thesis: verum

end;

assume Det (AutEqMt (f + ((- L) * (id V1))),b1,b1') = 0. K ; :: thesis: ( f is with_eigenvalues & L is eigenvalue of f )
then not ker (f + ((- L) * (id V1))) is trivial by A1, MATRLIN2:50;
hence ( f is with_eigenvalues & L is eigenvalue of f ) by Th14; :: thesis: verum