arity (1 proj 1) = 1 by COMPUT_1:41;
then dom [+] c= (1 + 1) -tuples_on NAT by COMPUT_1:60;
hence dom [+] c= 2 -tuples_on NAT ; :: thesis: verum