theorem :: RELSET_3:62

for q, q1 being Rational holds [q1,(q1 * q)] in multRel (RAT,q)