for V being RealLinearSpace
for L being Linear_Combination of V
for A being Subset of V st A c= Carrier L holds
ex L1 being Linear_Combination of V st Carrier L1 = A by Lm7;