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