theorem :: RLVECT_2:60

for V being RealLinearSpace holds the addF of (LC_RLSpace V) = LCAdd V ;