theorem Th30: :: RLVECT_5:30

for V being finite-dimensional RealLinearSpace holds dim V = dim ((Omega). V)