for V being RealLinearSpace
for A, B being Subset of V
for l being Linear_Combination of A st A c= B holds
l is Linear_Combination of B