theorem lcsub: :: FIELD_6:46

for F being Field
for V being VectSp of F
for W being Subspace of V
for l1 being Linear_Combination of W ex l2 being Linear_Combination of V st
( Carrier l2 = Carrier l1 & ( for v being Element of V st v in Carrier l2 holds
l2 . v = l1 . v ) )