per cases ( g . x = {} or x in dom g ) by FUNCT_1:def 4;

suppose g . x = {} ; :: thesis: ( g . x is T-Sequence-like & g . x is Ordinal-yielding )

hence ( g . x is T-Sequence-like & g . x is Ordinal-yielding ) ; :: thesis: verum

end;

suppose x in dom g ; :: thesis: ( g . x is T-Sequence-like & g . x is Ordinal-yielding )

then g . x in rng g by FUNCT_1:def 5;
hence ( g . x is T-Sequence-like & g . x is Ordinal-yielding ) by OSV; :: thesis: verum

end;

end;