theorem :: RELSET_3:58

for r being Real holds multRel (REAL,r) = { [r1,(r1 * r)] where r1 is Real : verum }