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