for T being RealLinearSpace
for X being set holds
( X is Linear_Combination of RLSp2RVSp T iff X is Linear_Combination of T )