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;