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))

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

( 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

A4:
[#] REAL c= dom I
by FUNCT_2:def 1;
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;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

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