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
ex y being object st [#] V = {y} by A1, CARD_2:42;
hence [#] V = {(0. V)} by TARSKI:def 1; :: thesis: verum
end;
then (Omega). V = (0). V by VECTSP_4:def 3;
hence dim V = 0 by VECTSP_9:29; :: thesis: verum