theorem Th26: :: VECTSP_9:26

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