theorem Th9: :: VECTSP_9:9

for GF being Field
for V being VectSp of GF
for W being Subspace of V
for L being Linear_Combination of V st Carrier L c= the carrier of W holds
ex K being Linear_Combination of W st
( Carrier K = Carrier L & Sum K = Sum L )