theorem Th13: :: VECTSP10:13
for K being Field
for V being VectSp of K
for W being Subspace of V
for v being Vector of V
for w being Vector of W st v = w holds
Lin {w} = Lin {v}