let x0 be 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*> )
let I be Function of REAL,(REAL-NS 1); ( I = (proj (1,1)) " implies ( I is_differentiable_in x0 & diff (I,x0) = <*1*> ) )
assume A1:
I = (proj (1,1)) "
; ( I is_differentiable_in x0 & diff (I,x0) = <*1*> )
I . jj = <*jj*>
by A1, PDIFF_1:1;
then reconsider r = <*jj*> as Point of (REAL-NS 1) ;
A2:
for x being Real st x in [#] REAL holds
I /. x = (x * r) + (0. (REAL-NS 1))
A4:
[#] REAL c= dom I
by FUNCT_2:def 1;
then A5:
( I is_differentiable_on [#] REAL & ( for x being Real st x in [#] REAL holds
(I `| ([#] REAL)) . x = r ) )
by A2, NDIFF_3:21;
A6:
x0 in [#] REAL
by XREAL_0:def 1;
hence
I is_differentiable_in x0
by A5, NDIFF_3:10; diff (I,x0) = <*1*>
r =
(I `| ([#] REAL)) . x0
by A4, A2, A6, NDIFF_3:21
.=
diff (I,x0)
by A5, A6, NDIFF_3:def 6
;
hence
diff (I,x0) = <*1*>
; verum