theorem Th23: :: RLVECT_2:23

for V being RealLinearSpace
for l being Linear_Combination of {} the carrier of V holds l = ZeroLC V