let X be RealBanachSpace; :: thesis: for Z being open Subset of REAL

for a, b being Real

for y0 being VECTOR of X

for G being Function of X,X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X holds

ex y being continuous PartFunc of REAL, the carrier of X st

( dom y = ['a,b'] & y is_differentiable_on Z & y /. a = y0 & ( for t being Real st t in Z holds

diff (y,t) = G . (y /. t) ) )

let Z be open Subset of REAL; :: thesis: for a, b being Real

for y0 being VECTOR of X

for G being Function of X,X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X holds

ex y being continuous PartFunc of REAL, the carrier of X st

( dom y = ['a,b'] & y is_differentiable_on Z & y /. a = y0 & ( for t being Real st t in Z holds

diff (y,t) = G . (y /. t) ) )

let a, b be Real; :: thesis: for y0 being VECTOR of X

for G being Function of X,X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X holds

ex y being continuous PartFunc of REAL, the carrier of X st

( dom y = ['a,b'] & y is_differentiable_on Z & y /. a = y0 & ( for t being Real st t in Z holds

diff (y,t) = G . (y /. t) ) )

let y0 be VECTOR of X; :: thesis: for G being Function of X,X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X holds

ex y being continuous PartFunc of REAL, the carrier of X st

( dom y = ['a,b'] & y is_differentiable_on Z & y /. a = y0 & ( for t being Real st t in Z holds

diff (y,t) = G . (y /. t) ) )

let G be Function of X,X; :: thesis: ( a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X implies ex y being continuous PartFunc of REAL, the carrier of X st

( dom y = ['a,b'] & y is_differentiable_on Z & y /. a = y0 & ( for t being Real st t in Z holds

diff (y,t) = G . (y /. t) ) ) )

assume A1: ( a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X ) ; :: thesis: ex y being continuous PartFunc of REAL, the carrier of X st

( dom y = ['a,b'] & y is_differentiable_on Z & y /. a = y0 & ( for t being Real st t in Z holds

diff (y,t) = G . (y /. t) ) )

then Fredholm (G,a,b,y0) is with_unique_fixpoint by Th57;

then consider x being set such that

A2: ( x is_a_fixpoint_of Fredholm (G,a,b,y0) & ( for y being set st y is_a_fixpoint_of Fredholm (G,a,b,y0) holds

x = y ) ) ;

( x in dom (Fredholm (G,a,b,y0)) & x = (Fredholm (G,a,b,y0)) . x ) by A2;

then reconsider x = x as Element of the carrier of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) ;

consider f being continuous PartFunc of REAL, the carrier of X such that

A4: ( x = f & dom f = ['a,b'] ) by ORDEQ_01:def 2;

take f ; :: thesis: ( dom f = ['a,b'] & f is_differentiable_on Z & f /. a = y0 & ( for t being Real st t in Z holds

diff (f,t) = G . (f /. t) ) )

thus ( dom f = ['a,b'] & f is_differentiable_on Z & f /. a = y0 ) by Th58, A4, A1, A2; :: thesis: for t being Real st t in Z holds

diff (f,t) = G . (f /. t)

A5: ].a,b.[ c= [.a,b.] by XXREAL_1:25;

A6: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;

let t be Real; :: thesis: ( t in Z implies diff (f,t) = G . (f /. t) )

assume A7: t in Z ; :: thesis: diff (f,t) = G . (f /. t)

dom G = the carrier of X by FUNCT_2:def 1;

then rng f c= dom G ;

then A8: dom (G * f) = ['a,b'] by A4, RELAT_1:27;

thus diff (f,t) = (G * f) /. t by A7, Th58, A4, A1, A2

.= (G * f) . t by A8, A5, A1, A7, A6, PARTFUN1:def 6

.= G . (f . t) by A8, A5, A1, A7, A6, FUNCT_1:12

.= G . (f /. t) by A5, A1, A7, A6, A4, PARTFUN1:def 6 ; :: thesis: verum

for a, b being Real

for y0 being VECTOR of X

for G being Function of X,X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X holds

ex y being continuous PartFunc of REAL, the carrier of X st

( dom y = ['a,b'] & y is_differentiable_on Z & y /. a = y0 & ( for t being Real st t in Z holds

diff (y,t) = G . (y /. t) ) )

let Z be open Subset of REAL; :: thesis: for a, b being Real

for y0 being VECTOR of X

for G being Function of X,X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X holds

ex y being continuous PartFunc of REAL, the carrier of X st

( dom y = ['a,b'] & y is_differentiable_on Z & y /. a = y0 & ( for t being Real st t in Z holds

diff (y,t) = G . (y /. t) ) )

let a, b be Real; :: thesis: for y0 being VECTOR of X

for G being Function of X,X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X holds

ex y being continuous PartFunc of REAL, the carrier of X st

( dom y = ['a,b'] & y is_differentiable_on Z & y /. a = y0 & ( for t being Real st t in Z holds

diff (y,t) = G . (y /. t) ) )

let y0 be VECTOR of X; :: thesis: for G being Function of X,X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X holds

ex y being continuous PartFunc of REAL, the carrier of X st

( dom y = ['a,b'] & y is_differentiable_on Z & y /. a = y0 & ( for t being Real st t in Z holds

diff (y,t) = G . (y /. t) ) )

let G be Function of X,X; :: thesis: ( a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X implies ex y being continuous PartFunc of REAL, the carrier of X st

( dom y = ['a,b'] & y is_differentiable_on Z & y /. a = y0 & ( for t being Real st t in Z holds

diff (y,t) = G . (y /. t) ) ) )

assume A1: ( a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X ) ; :: thesis: ex y being continuous PartFunc of REAL, the carrier of X st

( dom y = ['a,b'] & y is_differentiable_on Z & y /. a = y0 & ( for t being Real st t in Z holds

diff (y,t) = G . (y /. t) ) )

then Fredholm (G,a,b,y0) is with_unique_fixpoint by Th57;

then consider x being set such that

A2: ( x is_a_fixpoint_of Fredholm (G,a,b,y0) & ( for y being set st y is_a_fixpoint_of Fredholm (G,a,b,y0) holds

x = y ) ) ;

( x in dom (Fredholm (G,a,b,y0)) & x = (Fredholm (G,a,b,y0)) . x ) by A2;

then reconsider x = x as Element of the carrier of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) ;

consider f being continuous PartFunc of REAL, the carrier of X such that

A4: ( x = f & dom f = ['a,b'] ) by ORDEQ_01:def 2;

take f ; :: thesis: ( dom f = ['a,b'] & f is_differentiable_on Z & f /. a = y0 & ( for t being Real st t in Z holds

diff (f,t) = G . (f /. t) ) )

thus ( dom f = ['a,b'] & f is_differentiable_on Z & f /. a = y0 ) by Th58, A4, A1, A2; :: thesis: for t being Real st t in Z holds

diff (f,t) = G . (f /. t)

A5: ].a,b.[ c= [.a,b.] by XXREAL_1:25;

A6: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;

let t be Real; :: thesis: ( t in Z implies diff (f,t) = G . (f /. t) )

assume A7: t in Z ; :: thesis: diff (f,t) = G . (f /. t)

dom G = the carrier of X by FUNCT_2:def 1;

then rng f c= dom G ;

then A8: dom (G * f) = ['a,b'] by A4, RELAT_1:27;

thus diff (f,t) = (G * f) /. t by A7, Th58, A4, A1, A2

.= (G * f) . t by A8, A5, A1, A7, A6, PARTFUN1:def 6

.= G . (f . t) by A8, A5, A1, A7, A6, FUNCT_1:12

.= G . (f /. t) by A5, A1, A7, A6, A4, PARTFUN1:def 6 ; :: thesis: verum