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

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;

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

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

end;

end;