for V being RealLinearSpace holds the carrier of (LC_RLSpace V) = LinComb V ;