A1: arity g = 2 by Def26;
g is non empty homogeneous quasi_total PartFunc of (NAT * ),NAT by Th20;
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 G' = G as non empty homogeneous quasi_total PartFunc of (NAT * ),NAT by A4;
G' is non empty NAT * -defined to-naturals homogeneous len-total ternary Function by A3, Def27;
hence ( not (1,2)->(1,?,2) g is empty & (1,2)->(1,?,2) g is ternary & (1,2)->(1,?,2) g is len-total ) by A2; :: thesis: verum