theorem :: NDIFF_4:37

for x0 being Real
for I being Function of REAL,(REAL-NS 1) st I = (proj (1,1)) " holds
( I is_differentiable_in x0 & diff (I,x0) = <*1*> )