theorem Th13: :: RLVECT_5:13

for V being RealLinearSpace
for I being Basis of V
for v being VECTOR of V holds v in Lin I