theorem Th45: :: RLSUB_1:45

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