for V being RealLinearSpace holds 0. (LC_RLSpace V) = ZeroLC V ;