:: deftheorem Def3 defines eigenvector VECTSP11:def 3 :
for R being non empty doubleLoopStr
for V being non empty ModuleStr over R
for f being Function of V,V
for L being Scalar of R st f is with_eigenvalues & L is eigenvalue of f holds
for b₅ being Vector of V holds
( b₅ is eigenvector of f,L iff f . b₅ = L * b₅ );