theorem Th23: :: VECTSP_9:23

for GF being Field
for V being VectSp of GF holds (0). V is finite-dimensional