let F be Field; :: thesis: for V being finite-dimensional VectSp of F st card ([#] V) = 1 holds
dim V = 0
let V be finite-dimensional VectSp of F; :: thesis: ( card ([#] V) = 1 implies dim V = 0 )
assume A1: card ([#] V) = 1 ; :: thesis: dim V = 0
[#] V = {(0. V)}

proof

consider y being set such that
A2: [#] V = {y} by A1, CARD_2:60;
thus [#] V = {(0. V)} by A2, TARSKI:def 1; :: thesis: verum

end;

then (Omega). V = (0). V by VECTSP_4:def 3;
hence dim V = 0 by VECTSP_9:33; :: thesis: verum