let f be Morphism of a,b; :: thesis: ( f is Function-like & f is Relation-like )

per cases ( <^a,b^> <> {} or <^a,b^> = {} ) ;

suppose <^a,b^> <> {} ; :: thesis: ( f is Function-like & f is Relation-like )

hence ( f is Function-like & f is Relation-like ) by Th34; :: thesis: verum

end;

suppose <^a,b^> = {} ; :: thesis: ( f is Function-like & f is Relation-like )

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

end;

end;