let F be Field; :: thesis: for V being finite-dimensional VectSp of finite-dimensional holds dim ((0). V) = 0
let V be finite-dimensional VectSp of finite-dimensional ; :: thesis: dim ((0). V) = 0
(Omega). ((0). V) = (0). ((0). V) by VECTSP_4:47;
hence dim ((0). V) = 0 by VECTSP_9:33; :: thesis: verum