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

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

let x0 be Element of REAL 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 )

A2: 1 in Seg 1 ;

set R = (REAL 1) --> (0* 1);

set L = <>* J;

rng J = dom ((proj (1,1)) ") by A1, A2, PDIFF_1:1, PDIFF_1:2;

then A3: dom (<>* J) = dom J by RELAT_1:27

.= REAL 1 by A1, A2, PDIFF_1:1 ;

reconsider L = <>* J as Function of (REAL 1),(REAL 1) by PDIFF_1:2;

set f = <>* J;

A4: L = id (dom J) by A1, FUNCT_1:39

.= id (REAL 1) by A1, A2, PDIFF_1:1 ;

A5: for x, y being Element of REAL 1 holds L . (x + y) = (L . x) + (L . y) by A4;

A6: for x being Element of REAL 1

for r being Real holds L . (r * x) = r * (L . x) by A4;

then A7: L is LinearOperator of 1,1 by A5, PDIFF_6:def 1, PDIFF_6:def 2;

reconsider r0 = 1 as Real ;

A8: { y where y is Element of REAL 1 : |.(y - x0).| < r0 } c= dom (<>* J)

ex d being Real st

( d > 0 & ( for z, w being Element of REAL 1 st z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z holds

(|.z.| ") * |.w.| < r ) )

((<>* J) /. x) - ((<>* J) /. x0) = (L . (x - x0)) + (((REAL 1) --> (0* 1)) . (x - x0))

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

A13: rng J c= REAL ;

thus diff (J,x0) = (proj (1,1)) * L by A12, A7, A8, A9, PDIFF_6:24

.= ((proj (1,1)) * ((proj (1,1)) ")) * J by RELAT_1:36

.= (id (rng (proj (1,1)))) * J by FUNCT_1:39

.= (id REAL) * J by A2, PDIFF_1:1

.= J by A13, RELAT_1:53 ; :: thesis: verum

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

let x0 be Element of REAL 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 )

A2: 1 in Seg 1 ;

set R = (REAL 1) --> (0* 1);

set L = <>* J;

rng J = dom ((proj (1,1)) ") by A1, A2, PDIFF_1:1, PDIFF_1:2;

then A3: dom (<>* J) = dom J by RELAT_1:27

.= REAL 1 by A1, A2, PDIFF_1:1 ;

reconsider L = <>* J as Function of (REAL 1),(REAL 1) by PDIFF_1:2;

set f = <>* J;

A4: L = id (dom J) by A1, FUNCT_1:39

.= id (REAL 1) by A1, A2, PDIFF_1:1 ;

A5: for x, y being Element of REAL 1 holds L . (x + y) = (L . x) + (L . y) by A4;

A6: for x being Element of REAL 1

for r being Real holds L . (r * x) = r * (L . x) by A4;

then A7: L is LinearOperator of 1,1 by A5, PDIFF_6:def 1, PDIFF_6:def 2;

reconsider r0 = 1 as Real ;

A8: { y where y is Element of REAL 1 : |.(y - x0).| < r0 } c= dom (<>* J)

proof

A9:
for r being Real st r > 0 holds
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { y where y is Element of REAL 1 : |.(y - x0).| < r0 } or x in dom (<>* J) )

assume x in { y where y is Element of REAL 1 : |.(y - x0).| < r0 } ; :: thesis: x in dom (<>* J)

then ex y being Element of REAL 1 st

( x = y & |.(y - x0).| < r0 ) ;

hence x in dom (<>* J) by A3; :: thesis: verum

end;assume x in { y where y is Element of REAL 1 : |.(y - x0).| < r0 } ; :: thesis: x in dom (<>* J)

then ex y being Element of REAL 1 st

( x = y & |.(y - x0).| < r0 ) ;

hence x in dom (<>* J) by A3; :: thesis: verum

ex d being Real st

( d > 0 & ( for z, w being Element of REAL 1 st z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z holds

(|.z.| ") * |.w.| < r ) )

proof

A12:
for x being Element of REAL 1 st |.(x - x0).| < r0 holds
let r be Real; :: thesis: ( r > 0 implies ex d being Real st

( d > 0 & ( for z, w being Element of REAL 1 st z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z holds

(|.z.| ") * |.w.| < r ) ) )

assume A10: r > 0 ; :: thesis: ex d being Real st

( d > 0 & ( for z, w being Element of REAL 1 st z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z holds

(|.z.| ") * |.w.| < r ) )

take d = r; :: thesis: ( d > 0 & ( for z, w being Element of REAL 1 st z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z holds

(|.z.| ") * |.w.| < r ) )

thus 0 < d by A10; :: thesis: for z, w being Element of REAL 1 st z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z holds

(|.z.| ") * |.w.| < r

let z, w be Element of REAL 1; :: thesis: ( z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z implies (|.z.| ") * |.w.| < r )

assume A11: ( z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z ) ; :: thesis: (|.z.| ") * |.w.| < r

w = 0* 1 by A11, FUNCOP_1:7;

then |.w.| = 0 by EUCLID:7;

hence (|.z.| ") * |.w.| < r by A10; :: thesis: verum

end;( d > 0 & ( for z, w being Element of REAL 1 st z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z holds

(|.z.| ") * |.w.| < r ) ) )

assume A10: r > 0 ; :: thesis: ex d being Real st

( d > 0 & ( for z, w being Element of REAL 1 st z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z holds

(|.z.| ") * |.w.| < r ) )

take d = r; :: thesis: ( d > 0 & ( for z, w being Element of REAL 1 st z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z holds

(|.z.| ") * |.w.| < r ) )

thus 0 < d by A10; :: thesis: for z, w being Element of REAL 1 st z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z holds

(|.z.| ") * |.w.| < r

let z, w be Element of REAL 1; :: thesis: ( z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z implies (|.z.| ") * |.w.| < r )

assume A11: ( z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z ) ; :: thesis: (|.z.| ") * |.w.| < r

w = 0* 1 by A11, FUNCOP_1:7;

then |.w.| = 0 by EUCLID:7;

hence (|.z.| ") * |.w.| < r by A10; :: thesis: verum

((<>* J) /. x) - ((<>* J) /. x0) = (L . (x - x0)) + (((REAL 1) --> (0* 1)) . (x - x0))

proof

then
( <>* J is_differentiable_in x0 & diff ((<>* J),x0) = L )
by A7, A8, A9, PDIFF_6:24;
let x be Element of REAL 1; :: thesis: ( |.(x - x0).| < r0 implies ((<>* J) /. x) - ((<>* J) /. x0) = (L . (x - x0)) + (((REAL 1) --> (0* 1)) . (x - x0)) )

assume |.(x - x0).| < r0 ; :: thesis: ((<>* J) /. x) - ((<>* J) /. x0) = (L . (x - x0)) + (((REAL 1) --> (0* 1)) . (x - x0))

thus ((<>* J) /. x) - ((<>* J) /. x0) = (L /. x) - (L /. x0)

.= (L /. x) + (L /. ((- 1) * x0)) by A6

.= L . (x - x0) by A5

.= (L . (x - x0)) + (0* 1) by RVSUM_1:16

.= (L . (x - x0)) + (((REAL 1) --> (0* 1)) . (x - x0)) by FUNCOP_1:7 ; :: thesis: verum

end;assume |.(x - x0).| < r0 ; :: thesis: ((<>* J) /. x) - ((<>* J) /. x0) = (L . (x - x0)) + (((REAL 1) --> (0* 1)) . (x - x0))

thus ((<>* J) /. x) - ((<>* J) /. x0) = (L /. x) - (L /. x0)

.= (L /. x) + (L /. ((- 1) * x0)) by A6

.= L . (x - x0) by A5

.= (L . (x - x0)) + (0* 1) by RVSUM_1:16

.= (L . (x - x0)) + (((REAL 1) --> (0* 1)) . (x - x0)) by FUNCOP_1:7 ; :: thesis: verum

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

A13: rng J c= REAL ;

thus diff (J,x0) = (proj (1,1)) * L by A12, A7, A8, A9, PDIFF_6:24

.= ((proj (1,1)) * ((proj (1,1)) ")) * J by RELAT_1:36

.= (id (rng (proj (1,1)))) * J by FUNCT_1:39

.= (id REAL) * J by A2, PDIFF_1:1

.= J by A13, RELAT_1:53 ; :: thesis: verum