let P be Relation; :: thesis: ( P is x -valued implies P is Function-like )

per cases ( x = {} or not x = {} ) ;

suppose A1: x = {} ; :: thesis: ( P is x -valued implies P is Function-like )

assume P is x -valued ; :: thesis: P is Function-like
hence P is Function-like by A1; :: thesis: verum

end;

suppose A2: not x = {} ; :: thesis: ( P is x -valued implies P is Function-like )

assume P is x -valued ; :: thesis: P is Function-like
hence P is Function-like by Lm80, A2; :: thesis: verum

end;

end;