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

for f, g being continuous PartFunc of REAL, the carrier of X st dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & a < b & G is_Lipschitzian_on the carrier of X & g = (Fredholm (G,a,b,y0)) . f holds

( g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds

diff (g,t) = (G * f) /. 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

for f, g being continuous PartFunc of REAL, the carrier of X st dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & a < b & G is_Lipschitzian_on the carrier of X & g = (Fredholm (G,a,b,y0)) . f holds

( g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds

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

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

for G being Function of X,X

for f, g being continuous PartFunc of REAL, the carrier of X st dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & a < b & G is_Lipschitzian_on the carrier of X & g = (Fredholm (G,a,b,y0)) . f holds

( g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds

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

let y0 be VECTOR of X; :: thesis: for G being Function of X,X

for f, g being continuous PartFunc of REAL, the carrier of X st dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & a < b & G is_Lipschitzian_on the carrier of X & g = (Fredholm (G,a,b,y0)) . f holds

( g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds

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

let G be Function of X,X; :: thesis: for f, g being continuous PartFunc of REAL, the carrier of X st dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & a < b & G is_Lipschitzian_on the carrier of X & g = (Fredholm (G,a,b,y0)) . f holds

( g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds

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

let f, g be continuous PartFunc of REAL, the carrier of X; :: thesis: ( dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & a < b & G is_Lipschitzian_on the carrier of X & g = (Fredholm (G,a,b,y0)) . f implies ( g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds

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

assume A1: ( dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & a < b & G is_Lipschitzian_on the carrier of X & g = (Fredholm (G,a,b,y0)) . f ) ; :: thesis: ( g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds

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

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

set D = R_NormSpace_of_ContinuousFunctions (['a,b'],X);

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

then A2: G is_continuous_on dom G by A1, NFCONT_1:45;

f is Element of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) by ORDEQ_01:def 2, A1;

then consider f0, g0, Gf0 being continuous PartFunc of REAL, the carrier of X such that

A3: ( f = f0 & (Fredholm (G,a,b,y0)) . f = g0 & dom f0 = ['a,b'] & dom g0 = ['a,b'] & Gf0 = G * f0 & ( for t being Real st t in ['a,b'] holds

g0 /. t = y0 + (integral (Gf0,a,t)) ) ) by A1, A2, Def8;

reconsider Gf = G * f as continuous PartFunc of REAL, the carrier of X by A3;

rng f c= dom G by X2;

then dom Gf = ['a,b'] by A1, RELAT_1:27;

hence ( g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds

diff (g,t) = (G * f) /. t ) ) by A1, X1, Th40, Th40a, A3; :: thesis: verum

for a, b being Real

for y0 being VECTOR of X

for G being Function of X,X

for f, g being continuous PartFunc of REAL, the carrier of X st dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & a < b & G is_Lipschitzian_on the carrier of X & g = (Fredholm (G,a,b,y0)) . f holds

( g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds

diff (g,t) = (G * f) /. 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

for f, g being continuous PartFunc of REAL, the carrier of X st dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & a < b & G is_Lipschitzian_on the carrier of X & g = (Fredholm (G,a,b,y0)) . f holds

( g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds

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

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

for G being Function of X,X

for f, g being continuous PartFunc of REAL, the carrier of X st dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & a < b & G is_Lipschitzian_on the carrier of X & g = (Fredholm (G,a,b,y0)) . f holds

( g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds

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

let y0 be VECTOR of X; :: thesis: for G being Function of X,X

for f, g being continuous PartFunc of REAL, the carrier of X st dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & a < b & G is_Lipschitzian_on the carrier of X & g = (Fredholm (G,a,b,y0)) . f holds

( g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds

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

let G be Function of X,X; :: thesis: for f, g being continuous PartFunc of REAL, the carrier of X st dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & a < b & G is_Lipschitzian_on the carrier of X & g = (Fredholm (G,a,b,y0)) . f holds

( g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds

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

let f, g be continuous PartFunc of REAL, the carrier of X; :: thesis: ( dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & a < b & G is_Lipschitzian_on the carrier of X & g = (Fredholm (G,a,b,y0)) . f implies ( g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds

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

assume A1: ( dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & a < b & G is_Lipschitzian_on the carrier of X & g = (Fredholm (G,a,b,y0)) . f ) ; :: thesis: ( g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds

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

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

set D = R_NormSpace_of_ContinuousFunctions (['a,b'],X);

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

then A2: G is_continuous_on dom G by A1, NFCONT_1:45;

f is Element of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) by ORDEQ_01:def 2, A1;

then consider f0, g0, Gf0 being continuous PartFunc of REAL, the carrier of X such that

A3: ( f = f0 & (Fredholm (G,a,b,y0)) . f = g0 & dom f0 = ['a,b'] & dom g0 = ['a,b'] & Gf0 = G * f0 & ( for t being Real st t in ['a,b'] holds

g0 /. t = y0 + (integral (Gf0,a,t)) ) ) by A1, A2, Def8;

reconsider Gf = G * f as continuous PartFunc of REAL, the carrier of X by A3;

rng f c= dom G by X2;

then dom Gf = ['a,b'] by A1, RELAT_1:27;

hence ( g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds

diff (g,t) = (G * f) /. t ) ) by A1, X1, Th40, Th40a, A3; :: thesis: verum