theorem Th64: :: CLVECT_1:64

for V being ComplexLinearSpace
for v being VECTOR of V holds v + ((0). V) = {v}