for V being RealLinearSpace
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}