theorem :: VECTSP_9:38

for GF being Field
for n being Nat
for V being finite-dimensional VectSp of GF
for W being Subspace of V holds n Subspaces_of W c= n Subspaces_of V