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)}

hence dim V = 0 by VECTSP_9:29; :: thesis: verum

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

then
(Omega). V = (0). V
by VECTSP_4:def 3;
ex y being object st [#] V = {y}
by A1, CARD_2:42;

hence [#] V = {(0. V)} by TARSKI:def 1; :: thesis: verum

end;hence [#] V = {(0. V)} by TARSKI:def 1; :: thesis: verum

hence dim V = 0 by VECTSP_9:29; :: thesis: verum