for F being Field
for V being VectSp of F st [#] V is finite holds
V is finite-dimensional