theorem Th13: :: RLTOPSP1:13

for X being RealLinearSpace
for r being Real holds r * {(0. X)} = {(0. X)}