set G = (1,2)->(1,?,2) g;
dom <:<*(3 proj 1),(3 proj 3)*>:> = (dom (3 proj 1)) /\ (dom (3 proj 3)) by FUNCT_6:62;
then A1: dom <:<*(3 proj 1),(3 proj 3)*>:> = (3 -tuples_on NAT ) /\ (dom (3 proj 3)) by Th40
.= (3 -tuples_on NAT ) /\ (3 -tuples_on NAT ) by Th40
.= 3 -tuples_on NAT ;
A2: dom ((1,2)->(1,?,2) g) c= dom <:<*(3 proj 1),(3 proj 3)*>:> by RELAT_1:44;
3 -tuples_on NAT c= NAT * by MSUALG_1:12;
then A3: dom ((1,2)->(1,?,2) g) c= NAT * by A1, A2, XBOOLE_1:1;
thus ( (1,2)->(1,?,2) g is to-naturals & (1,2)->(1,?,2) g is NAT * -defined ) by A3, RELAT_1:def 18; :: thesis: verum