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