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