theorem :: RELSET_3:57

for r, r1 being Real holds [r1,(r1 * r)] in multRel (REAL,r)