theorem Th20: :: VECTSP_9:20

for GF being Field
for V being VectSp of GF st V is finite-dimensional holds
for I being Basis of V holds I is finite