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