set G = (1,2)->(1,?,2) g;
A1: 3 -tuples_on NAT c= NAT * by FINSEQ_2:142;
dom <:<*(3 proj 1),(3 proj 3)*>:> = (dom (3 proj 1)) /\ (dom (3 proj 3)) by FINSEQ_3:142;
then A2: dom <:<*(3 proj 1),(3 proj 3)*>:> = (3 -tuples_on NAT) /\ (dom (3 proj 3)) by Th35
.= (3 -tuples_on NAT) /\ (3 -tuples_on NAT) by Th35
.= 3 -tuples_on NAT ;
dom ((1,2)->(1,?,2) g) c= dom <:<*(3 proj 1),(3 proj 3)*>:> by RELAT_1:25;
then dom ((1,2)->(1,?,2) g) c= NAT * by A2, A1;
hence ( (1,2)->(1,?,2) g is to-naturals & (1,2)->(1,?,2) g is NAT * -defined ) ; :: thesis: verum