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 to-naturals homogeneous from-natural-fseqs 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