let F be Field; :: thesis: for V being finite-dimensional VectSp of F
for v being Vector of V st v <> 0. V holds
dim (Lin {v}) = 1
let V be finite-dimensional VectSp of F; :: thesis: for v being Vector of V st v <> 0. V holds
dim (Lin {v}) = 1
let v be Vector of V; :: thesis: ( v <> 0. V implies dim (Lin {v}) = 1 )
assume A1: v <> 0. V ; :: thesis: dim (Lin {v}) = 1
v in {v} by TARSKI:def 1;
then v in Lin {v} by VECTSP_7:13;
then reconsider v0 = v as Vector of (Lin {v}) by STRUCT_0:def 5;
A2: Lin {v0} = Lin {v} by VECTSP_9:21;
A3: v <> 0. (Lin {v}) by A1, VECTSP_4:19;
(Omega). (Lin {v0}) = Lin {v0} ;
hence dim (Lin {v}) = 1 by A2, A3, VECTSP_9:34; :: thesis: verum