theorem Th6: :: VECTSP_9:6

for GF being Field
for V being VectSp of GF
for L being Linear_Combination of V
for A being Subset of V st Carrier L c= the carrier of (Lin A) holds
ex K being Linear_Combination of A st Sum L = Sum K