per cases ( x in dom g or not x in dom g ) ;

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

then reconsider x = x as Element of NAT ;
( 1 <= x & x <= len g ) by A1, FINSEQ_3:25;
hence ( g . x is Function-like & g . x is Relation-like ) by Def6; :: thesis: verum

end;

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

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

end;

end;