for J being Function of (REAL-NS 1),REAL
for x0 being Point of (REAL-NS 1) st J = proj (1,1) holds
( J is_differentiable_in x0 & diff (J,x0) = J )