for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L1, L2 being Scalar of K st f is with_eigenvalues & L1 <> L2 & L2 is eigenvalue of f holds
for I being Linear_Compl of UnionKers (f + ((- L1) * (id V1)))
for fI being linear-transformation of I,I st fI = f | I holds
( fI is with_eigenvalues & L1 is not eigenvalue of fI & L2 is eigenvalue of fI & UnionKers (f + ((- L2) * (id V1))) is Subspace of I )