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 & (id V) . v = L * v ) by Def2;
L * v = v by A1, FUNCT_1:34
.= (1_ K) * v by VECTSP_1:def 26 ;
hence L = 1_ K by A1, VECTSP10:5; :: thesis: verum