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

suppose g . x = {} ; :: thesis: ( g . x is Relation-like & g . x is Function-like )

hence ( g . x is Relation-like & g . x is Function-like ) ; :: thesis: verum

end;

suppose x in dom g ; :: thesis: ( g . x is Relation-like & g . x is Function-like )

then g . x in rng g by FUNCT_1:def 3;
hence ( g . x is Relation-like & g . x is Function-like ) by Def9; :: thesis: verum

end;

end;