n in NAT by ORDINAL1:def 12;
then [n,n] in [:NAT,NAT:] by ZFMISC_1:87;
then [n,n] in dom addnat by FUNCT_2:def 1;
then n in dom (curry addnat) by FUNCT_5:19;
hence ( (curry addnat) . n is Function-like & (curry addnat) . n is Relation-like ) by FUNCT_5:30; :: thesis: verum