for K being Field
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))) )