theorem :: VECTSP12:11

for K being Field
for V being finite-dimensional VectSp of K
for W being Subspace of V holds
( VectQuot (V,W) is finite-dimensional & (dim (VectQuot (V,W))) + (dim W) = dim V )