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 and
A3: f . v = L * v by Def2;
A4: (a * f) . v = a * (L * v) by A3, MATRLIN:def 4
.= (a * L) * v by VECTSP_1:def 16 ;
hence A5: a * f is with_eigenvalues by A2; :: 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 ) )
hence A6: a * L is eigenvalue of a * f by A2, 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 A7: w is eigenvector of f,L ; :: thesis: w is eigenvector of a * f,a * L
(a * f) . w = a * (f . w) by MATRLIN:def 4
.= a * (L * w) by A7, Def3
.= (a * L) * w by VECTSP_1:def 16 ;
hence w is eigenvector of a * f,a * L by A5, A6, Def3; :: thesis: verum

end;

assume A8: w is eigenvector of a * f,a * L ; :: thesis: w is eigenvector of f,L
a * (f . w) = (a * f) . w by MATRLIN:def 4
.= (a * L) * w by A5, A6, A8, Def3
.= a * (L * w) by VECTSP_1:def 16 ;
then 0. V = (a * (f . w)) + (- (a * (L * w))) by VECTSP_1:16
.= (a * (f . w)) + (a * (- (L * w))) by VECTSP_1:22
.= a * ((f . w) - (L * w)) by VECTSP_1:def 14 ;
then (f . w) - (L * w) = 0. V by A1, VECTSP_1:15;
then - (f . w) = - (L * w) by VECTSP_1:16;
then f . w = L * w by RLVECT_1:18;
hence w is eigenvector of f,L by Def3; :: thesis: verum