theorem :: RELSET_3:72

for n, n1 being Nat holds [n1,(n1 * n)] in multRel (NAT,n)