let x0 be Real; :: thesis: 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); :: thesis: ( I = (proj (1,1)) " implies ( I is_differentiable_in x0 & diff (I,x0) = <*1*> ) )
assume A1: I = (proj (1,1)) " ; :: thesis: ( 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))
proof
let x be Real; :: thesis: ( x in [#] REAL implies I /. x = (x * r) + (0. (REAL-NS 1)) )
reconsider xx = x as Element of REAL by XREAL_0:def 1;
assume x in [#] REAL ; :: thesis: I /. x = (x * r) + (0. (REAL-NS 1))
I . jj in REAL 1 by A1, FUNCT_1:3, PDIFF_1:2;
then A3: <*1*> is Element of REAL 1 by A1, PDIFF_1:1;
I /. xx = <*(x * 1)*> by A1, PDIFF_1:1
.= x * <*1*> by RVSUM_1:47 ;
hence I /. x = x * r by A3, REAL_NS1:3
.= (x * r) + (0. (REAL-NS 1)) by RLVECT_1:4 ;
:: thesis: verum
end;
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; :: thesis: 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*> ; :: thesis: verum