theorem :: VECTSP_9:28

for GF being Field
for V being finite-dimensional VectSp of GF
for W being Subspace of V holds
( dim V = dim W iff (Omega). V = (Omega). W )