let K be Field; :: thesis: for V being non trivial VectSp of K holds
( id V is with_eigenvalues & ex v being Vector of V st
( v <> 0. V & (id V) . v = (1_ K) * v ) )
let V be non trivial VectSp of K; :: thesis: ( id V is with_eigenvalues & ex v being Vector of V st
( v <> 0. V & (id V) . v = (1_ K) * v ) )
consider v being Vector of V such that
A1: v <> 0. V by STRUCT_0:def 18;
(id V) . v = v
.= (1_ K) * v ;
hence ( id V is with_eigenvalues & ex v being Vector of V st
( v <> 0. V & (id V) . v = (1_ K) * v ) ) by A1; :: thesis: verum