for G being Field
for V being VectSp of G
for A being Subset of V st A is linearly-independent holds
A is Basis of (Lin A)