theorem :: RLVECT_5:24

for V being RealLinearSpace st V is finite-dimensional holds
for A being Subset of V st A is linearly-independent holds
A is finite