let n be non zero Element of NAT ; :: thesis: for a, b being Real
for Z being open Subset of REAL
for y0 being VECTOR of (REAL-NS n)
for G being Function of (REAL-NS n),(REAL-NS n)
for y being continuous PartFunc of REAL,(REAL-NS n) st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of (REAL-NS n) & 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 Z being open Subset of REAL
for y0 being VECTOR of (REAL-NS n)
for G being Function of (REAL-NS n),(REAL-NS n)
for y being continuous PartFunc of REAL,(REAL-NS n) st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of (REAL-NS n) & 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 y0 being VECTOR of (REAL-NS n)
for G being Function of (REAL-NS n),(REAL-NS n)
for y being continuous PartFunc of REAL,(REAL-NS n) st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of (REAL-NS n) & 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 (REAL-NS n); :: thesis: for G being Function of (REAL-NS n),(REAL-NS n)
for y being continuous PartFunc of REAL,(REAL-NS n) st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of (REAL-NS n) & 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 (REAL-NS n),(REAL-NS n); :: thesis: for y being continuous PartFunc of REAL,(REAL-NS n) st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of (REAL-NS n) & 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,(REAL-NS n); :: thesis: ( a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of (REAL-NS n) & 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 (REAL-NS n) & 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)
A2: dom (Fredholm (G,a,b,y0)) = the carrier of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))) by FUNCT_2:def 1;
A3: y is Element of the carrier of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))) by Def2, A1;
A4: y in dom (Fredholm (G,a,b,y0)) by A2, Def2, A1;
dom G = the carrier of (REAL-NS n) 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,(REAL-NS n) 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 Def7, A1, A3;
dom G = the carrier of (REAL-NS n) by FUNCT_2:def 1;
then rng f c= dom G ;
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; :: thesis: ( t in Z implies diff (y,t) = Gf /. t )
assume A7: t in Z ; :: thesis: diff (y,t) = Gf /. t
A8: ].a,b.[ c= [.a,b.] by XXREAL_1:25;
A9: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
thus diff (y,t) = G . (y /. t) by A1, A7
.= G . (y . t) by A8, A1, A7, A9, PARTFUN1:def 6
.= Gf . t by A5, A8, A1, A7, A9, FUNCT_1:13
.= Gf /. t by A5, A8, A1, A7, A9, A6, PARTFUN1:def 6 ; :: thesis: verum

end;

hence y is_a_fixpoint_of Fredholm (G,a,b,y0) by A4, A5, Th43, A1, A6; :: thesis: verum