theorem :: RLVECT_2:34

for V being RealLinearSpace
for L being Linear_Combination of V st Carrier L = {} holds
Sum L = 0. V