let K be Field; :: thesis: for V being non trivial VectSp of K
for L being eigenvalue of id V holds L = 1_ K
let V be non trivial VectSp of K; :: thesis: for L being eigenvalue of id V holds L = 1_ K
let L be eigenvalue of id V; :: thesis: L = 1_ K
id V is with_eigenvalues by Th11;
then consider v being Vector of V such that
A1: v <> 0. V and
A2: (id V) . v = L * v by Def2;
L * v = v by A2
.= (1_ K) * v ;
hence L = 1_ K by A1, VECTSP10:4; :: thesis: verum