let K be Field; :: thesis: for V being non trivial VectSp of K
for w being Vector of V
for a being Element of K st a <> 0. K holds
for f being with_eigenvalues Function of V,V
for L being eigenvalue of f holds
( a * f is with_eigenvalues & a * L is eigenvalue of a * f & ( w is eigenvector of f,L implies w is eigenvector of a * f,a * L ) & ( w is eigenvector of a * f,a * L implies w is eigenvector of f,L ) )
let V be non trivial VectSp of K; :: thesis: for w being Vector of V
for a being Element of K st a <> 0. K holds
for f being with_eigenvalues Function of V,V
for L being eigenvalue of f holds
( a * f is with_eigenvalues & a * L is eigenvalue of a * f & ( w is eigenvector of f,L implies w is eigenvector of a * f,a * L ) & ( w is eigenvector of a * f,a * L implies w is eigenvector of f,L ) )
let w be Vector of V; :: thesis: for a being Element of K st a <> 0. K holds
for f being with_eigenvalues Function of V,V
for L being eigenvalue of f holds
( a * f is with_eigenvalues & a * L is eigenvalue of a * f & ( w is eigenvector of f,L implies w is eigenvector of a * f,a * L ) & ( w is eigenvector of a * f,a * L implies w is eigenvector of f,L ) )
let a be Element of K; :: thesis: ( a <> 0. K implies for f being with_eigenvalues Function of V,V
for L being eigenvalue of f holds
( a * f is with_eigenvalues & a * L is eigenvalue of a * f & ( w is eigenvector of f,L implies w is eigenvector of a * f,a * L ) & ( w is eigenvector of a * f,a * L implies w is eigenvector of f,L ) ) )
assume A1: a <> 0. K ; :: thesis: for f being with_eigenvalues Function of V,V
for L being eigenvalue of f holds
( a * f is with_eigenvalues & a * L is eigenvalue of a * f & ( w is eigenvector of f,L implies w is eigenvector of a * f,a * L ) & ( w is eigenvector of a * f,a * L implies w is eigenvector of f,L ) )
let f be with_eigenvalues Function of V,V; :: thesis: for L being eigenvalue of f holds
( a * f is with_eigenvalues & a * L is eigenvalue of a * f & ( w is eigenvector of f,L implies w is eigenvector of a * f,a * L ) & ( w is eigenvector of a * f,a * L implies w is eigenvector of f,L ) )
let L be eigenvalue of f; :: thesis: ( a * f is with_eigenvalues & a * L is eigenvalue of a * f & ( w is eigenvector of f,L implies w is eigenvector of a * f,a * L ) & ( w is eigenvector of a * f,a * L implies w is eigenvector of f,L ) )
consider v being Vector of V such that
A2: ( v <> 0. V & f . v = L * v ) by Def2;
A3: (a * f) . v = a * (L * v) by A2, MATRLIN:def 6
.= (a * L) * v by VECTSP_1:def 26 ;
hence A4: a * f is with_eigenvalues by A2, Def1; :: thesis: ( a * L is eigenvalue of a * f & ( w is eigenvector of f,L implies w is eigenvector of a * f,a * L ) & ( w is eigenvector of a * f,a * L implies w is eigenvector of f,L ) )
thus A5: a * L is eigenvalue of a * f by A2, A3, A4, Def2; :: thesis: ( ( w is eigenvector of f,L implies w is eigenvector of a * f,a * L ) & ( w is eigenvector of a * f,a * L implies w is eigenvector of f,L ) )

hereby :: thesis: ( w is eigenvector of a * f,a * L implies w is eigenvector of f,L )

assume A6: w is eigenvector of f,L ; :: thesis: w is eigenvector of a * f,a * L
(a * f) . w = a * (f . w) by MATRLIN:def 6
.= a * (L * w) by A6, Def3
.= (a * L) * w by VECTSP_1:def 26 ;
hence w is eigenvector of a * f,a * L by A4, A5, Def3; :: thesis: verum

end;

assume A7: w is eigenvector of a * f,a * L ; :: thesis: w is eigenvector of f,L
a * (f . w) = (a * f) . w by MATRLIN:def 6
.= (a * L) * w by A4, A5, A7, Def3
.= a * (L * w) by VECTSP_1:def 26 ;
then 0. V = (a * (f . w)) + (- (a * (L * w))) by VECTSP_1:63
.= (a * (f . w)) + (a * (- (L * w))) by VECTSP_1:69
.= a * ((f . w) - (L * w)) by VECTSP_1:def 26 ;
then (f . w) - (L * w) = 0. V by A1, VECTSP_1:60;
then - (f . w) = - (L * w) by VECTSP_1:63;
then f . w = L * w by RLVECT_1:31;
hence w is eigenvector of f,L by Def3; :: thesis: verum