theorem :: RELSET_3:36

for n being Nat
for X being natural-membered set holds addRel (X,n) = ((curry addnat) . n) |_2 X