for K being Field
for V being VectSp of K
for W being Subspace of V
for L being Linear_Combination of V holds L | the carrier of W is Linear_Combination of W