for V being RealLinearSpace
for L being Linear_Combination of V holds
( L + (ZeroLC V) = L & (ZeroLC V) + L = L )