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