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