theorem :: RELSET_3:71

for n1, n2 being Nat holds (multRel (NAT,n1)) * (multRel (NAT,n2)) = multRel (NAT,(n1 * n2))