theorem :: RELSET_3:56

for r1, r2 being Real holds (multRel (REAL,r1)) * (multRel (REAL,r2)) = multRel (REAL,(r1 * r2))