theorem Th39: :: RUSUB_1:39

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