theorem :: RLVECT_2:30

for V being RealLinearSpace holds Sum (ZeroLC V) = 0. V by Lm2;