theorem :: RELSET_3:63

for q being Rational holds multRel (RAT,q) = { [q1,(q1 * q)] where q1 is Rational : verum }