theorem Th23: :: RLVECT_5:23

for V being RealLinearSpace st V is finite-dimensional holds
for I being Basis of V holds I is finite