per cases ( g . x = {} or x in dom g ) by FUNCT_1:def 2;
suppose g . x = {} ; :: thesis: ( g . x is Sequence-like & g . x is Ordinal-yielding )
hence ( g . x is Sequence-like & g . x is Ordinal-yielding ) ; :: thesis: verum
end;
suppose x in dom g ; :: thesis: ( g . x is Sequence-like & g . x is Ordinal-yielding )
then g . x in rng g by FUNCT_1:def 3;
hence ( g . x is Sequence-like & g . x is Ordinal-yielding ) by Def9; :: thesis: verum
end;
end;