let J be Function of (REAL-NS 1),REAL; :: thesis: for x0 being Point of (REAL-NS 1) st J = proj (1,1) holds

( J is_differentiable_in x0 & diff (J,x0) = J )

let x0 be Point of (REAL-NS 1); :: thesis: ( J = proj (1,1) implies ( J is_differentiable_in x0 & diff (J,x0) = J ) )

assume A1: J = proj (1,1) ; :: thesis: ( J is_differentiable_in x0 & diff (J,x0) = J )

reconsider J0 = J as Function of (REAL 1),REAL by Lm1;

reconsider y0 = x0 as Element of REAL 1 by REAL_NS1:def 4;

( J0 is_differentiable_in y0 & diff (J0,y0) = J ) by A1, Th38;

hence J is_differentiable_in x0 ; :: thesis: diff (J,x0) = J

ex g being PartFunc of (REAL 1),REAL ex y being Element of REAL 1 st

( J = g & x0 = y & diff (J,x0) = diff (g,y) ) by Def7;

hence diff (J,x0) = J by A1, Th38; :: thesis: verum

( J is_differentiable_in x0 & diff (J,x0) = J )

let x0 be Point of (REAL-NS 1); :: thesis: ( J = proj (1,1) implies ( J is_differentiable_in x0 & diff (J,x0) = J ) )

assume A1: J = proj (1,1) ; :: thesis: ( J is_differentiable_in x0 & diff (J,x0) = J )

reconsider J0 = J as Function of (REAL 1),REAL by Lm1;

reconsider y0 = x0 as Element of REAL 1 by REAL_NS1:def 4;

( J0 is_differentiable_in y0 & diff (J0,y0) = J ) by A1, Th38;

hence J is_differentiable_in x0 ; :: thesis: diff (J,x0) = J

ex g being PartFunc of (REAL 1),REAL ex y being Element of REAL 1 st

( J = g & x0 = y & diff (J,x0) = diff (g,y) ) by Def7;

hence diff (J,x0) = J by A1, Th38; :: thesis: verum