theorem Th9: :: RUSUB_4:9

for V being finite-dimensional RealUnitarySpace
for A being Subset of V st A is linearly-independent holds
card A = dim (Lin A)