theorem :: RLVECT_2:58

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