for T being RealLinearSpace
for Lv being Linear_Combination of RLSp2RVSp T
for Lr being Linear_Combination of T st Lr = Lv holds
Carrier Lr = Carrier Lv