theorem VECT9Th26: :: ZMODUL06:60

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)