theorem :: RELSET_3:73

for n being Nat holds multRel (NAT,n) = { [n1,(n1 * n)] where n1 is Nat : verum }