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 y being continuous PartFunc of REAL, the carrier of X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X & 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) ) holds

y is_a_fixpoint_of Fredholm (G,a,b,y0)

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 y being continuous PartFunc of REAL, the carrier of X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X & 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) ) holds

y is_a_fixpoint_of Fredholm (G,a,b,y0)

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

for G being Function of X,X

for y being continuous PartFunc of REAL, the carrier of X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X & 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) ) holds

y is_a_fixpoint_of Fredholm (G,a,b,y0)

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

for y being continuous PartFunc of REAL, the carrier of X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X & 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) ) holds

y is_a_fixpoint_of Fredholm (G,a,b,y0)

let G be Function of X,X; :: thesis: for y being continuous PartFunc of REAL, the carrier of X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X & 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) ) holds

y is_a_fixpoint_of Fredholm (G,a,b,y0)

let y be continuous PartFunc of REAL, the carrier of X; :: thesis: ( a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X & 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) ) implies y is_a_fixpoint_of Fredholm (G,a,b,y0) )

assume A1: ( a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X & 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) ) ) ; :: thesis: y is_a_fixpoint_of Fredholm (G,a,b,y0)

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

A2: dom (Fredholm (G,a,b,y0)) = the carrier of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) by FUNCT_2:def 1;

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

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

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

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

A5: ( y = f & (Fredholm (G,a,b,y0)) . y = g & dom f = ['a,b'] & dom g = ['a,b'] & Gf = G * f & ( for t being Real st t in ['a,b'] holds

g /. t = y0 + (integral (Gf,a,t)) ) ) by Def8, A1, A3;

rng f c= dom G by X2;

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

for t being Real st t in Z holds

diff (y,t) = Gf /. t

for a, b being Real

for y0 being VECTOR of X

for G being Function of X,X

for y being continuous PartFunc of REAL, the carrier of X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X & 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) ) holds

y is_a_fixpoint_of Fredholm (G,a,b,y0)

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 y being continuous PartFunc of REAL, the carrier of X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X & 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) ) holds

y is_a_fixpoint_of Fredholm (G,a,b,y0)

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

for G being Function of X,X

for y being continuous PartFunc of REAL, the carrier of X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X & 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) ) holds

y is_a_fixpoint_of Fredholm (G,a,b,y0)

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

for y being continuous PartFunc of REAL, the carrier of X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X & 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) ) holds

y is_a_fixpoint_of Fredholm (G,a,b,y0)

let G be Function of X,X; :: thesis: for y being continuous PartFunc of REAL, the carrier of X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X & 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) ) holds

y is_a_fixpoint_of Fredholm (G,a,b,y0)

let y be continuous PartFunc of REAL, the carrier of X; :: thesis: ( a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X & 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) ) implies y is_a_fixpoint_of Fredholm (G,a,b,y0) )

assume A1: ( a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X & 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) ) ) ; :: thesis: y is_a_fixpoint_of Fredholm (G,a,b,y0)

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

A2: dom (Fredholm (G,a,b,y0)) = the carrier of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) by FUNCT_2:def 1;

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

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

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

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

A5: ( y = f & (Fredholm (G,a,b,y0)) . y = g & dom f = ['a,b'] & dom g = ['a,b'] & Gf = G * f & ( for t being Real st t in ['a,b'] holds

g /. t = y0 + (integral (Gf,a,t)) ) ) by Def8, A1, A3;

rng f c= dom G by X2;

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

for t being Real st t in Z holds

diff (y,t) = Gf /. t

proof

hence
y is_a_fixpoint_of Fredholm (G,a,b,y0)
by A1, X1, A2, A5, Th47, A6, ORDEQ_01:def 2; :: thesis: verum
let t be Real; :: thesis: ( t in Z implies diff (y,t) = Gf /. t )

assume A7: t in Z ; :: thesis: diff (y,t) = Gf /. t

hence diff (y,t) = G . (y /. t) by A1

.= G . (y . t) by A1, A7, PARTFUN1:def 6

.= Gf . t by A5, A1, A7, FUNCT_1:13

.= Gf /. t by A5, A1, A7, A6, PARTFUN1:def 6 ;

:: thesis: verum

end;assume A7: t in Z ; :: thesis: diff (y,t) = Gf /. t

hence diff (y,t) = G . (y /. t) by A1

.= G . (y . t) by A1, A7, PARTFUN1:def 6

.= Gf . t by A5, A1, A7, FUNCT_1:13

.= Gf /. t by A5, A1, A7, A6, PARTFUN1:def 6 ;

:: thesis: verum