theorem Th8: :: VECTSP_9:8

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