set G = (1,2)->(1,?,2) g;
dom <:<*(3 proj 1),(3 proj 3)*>:> = (dom (3 proj 1)) /\ (dom (3 proj 3)) by FINSEQ_3:142;
then 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 ;
then dom ((1,2)->(1,?,2) g) c= 3 -tuples_on NAT by RELAT_1:25;
hence dom ((1,2)->(1,?,2) g) is with_common_domain ; :: according to MARGREL1:def 21 :: thesis: verum