for r, s being Real holds s * |[r]| = |[(s * r)]| by RVSUM_1:47;