for K being Field
for V being non trivial VectSp of K
for f1, f2 being with_eigenvalues Function of V,V
for L1, L2 being Scalar of K st L1 is eigenvalue of f1 & L2 is eigenvalue of f2 & ex v being Vector of V st
( v is eigenvector of f1,L1 & v is eigenvector of f2,L2 & v <> 0. V ) holds
( f1 + f2 is with_eigenvalues & L1 + L2 is eigenvalue of f1 + f2 & ( for w being Vector of V st w is eigenvector of f1,L1 & w is eigenvector of f2,L2 holds
w is eigenvector of f1 + f2,L1 + L2 ) )