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 A1: F . x in rng F by Def3;
rng F c= A by RELAT_1:def 19;
hence ( F . x is Function-like & F . x is Relation-like ) by A1; :: 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 Def2; :: thesis: verum

end;

end;