theorem Th10: :: VECTSP_9:10
for GF being Field
for V being VectSp of GF
for I being Basis of V
for v being Vector of V holds v in Lin I