theorem Th27: :: VECTSP_9:27

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