Can anyone check if this argument works. I just made up this problem to check if I understand whats going on. Consider F = xy*e^x + y*e^y = K. I want to see if there is a unique solution. Fy = x*e^x + y*e^y + e^y. Since we are on the surface x*e^x + y*e^y = K. So if K >= 0 then Fy ≠ 0. So given any x we can find a unique y. Did I understand the theorem correctly?