theorem :: RLVECT_2:59

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