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 v <> 0. V ; :: thesis: dim (Lin {v}) = 1
then A1: v <> 0. (Lin {v}) by VECTSP_4:11;
v in {v} by TARSKI:def 1;
then v in Lin {v} by VECTSP_7:8;
then reconsider v0 = v as Vector of (Lin {v}) ;
( Lin {v0} = Lin {v} & (Omega). (Lin {v0}) = Lin {v0} ) by VECTSP_9:17;
hence dim (Lin {v}) = 1 by A1, VECTSP_9:30; :: thesis: verum