theorem :: RLVECT_2:31

for V being RealLinearSpace
for l being Linear_Combination of {} the carrier of V holds Sum l = 0. V