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

end;

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

then
f . x in rng f
by FUNCT_1:def 3;

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

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