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