let X be RealBanachSpace; 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; 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; 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; 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; 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; ( 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) ) )
; 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
let t be
Real;
( t in Z implies diff (y,t) = Gf /. t )
assume A7:
t in Z
;
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
;
verum
end;
hence
y is_a_fixpoint_of Fredholm (G,a,b,y0)
by A1, X1, A2, A5, Th47, A6, ORDEQ_01:def 2; verum