for K being Field
for V being VectSp of K
for A being finite Subset of V holds dim (Lin A) <= card A