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