theorem :: RELSET_3:38

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