A1: g is non empty homogeneous quasi_total PartFunc of (NAT *),NAT by Th16;
arity g = 2 by Def21;
then consider G being homogeneous PartFunc of (NAT *),NAT such that
A2: G = g * <:<*(3 proj 1),(3 proj 3)*>:> and
G is Element of HFuncs NAT and
A3: arity G = 3 and
A4: ( G is quasi_total & not G is empty ) by A1, Lm8;
reconsider G9 = G as non empty homogeneous quasi_total PartFunc of (NAT *),NAT by A4;
G9 is non empty NAT * -defined to-naturals homogeneous len-total 3 -ary Function by A3, Def21;
hence ( not (1,2)->(1,?,2) g is empty & (1,2)->(1,?,2) g is 3 -ary & (1,2)->(1,?,2) g is len-total ) by A2; :: thesis: verum