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