let n be non zero Element of NAT ; 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) st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of (REAL-NS n) holds
ex y being continuous PartFunc of REAL,(REAL-NS n) st
( 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) ) )
let a, b be 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) st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of (REAL-NS n) holds
ex y being continuous PartFunc of REAL,(REAL-NS n) st
( 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) ) )
let Z be open Subset of REAL; for y0 being VECTOR of (REAL-NS n)
for G being Function of (REAL-NS n),(REAL-NS n) st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of (REAL-NS n) holds
ex y being continuous PartFunc of REAL,(REAL-NS n) st
( 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) ) )
let y0 be VECTOR of (REAL-NS n); for G being Function of (REAL-NS n),(REAL-NS n) st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of (REAL-NS n) holds
ex y being continuous PartFunc of REAL,(REAL-NS n) st
( 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) ) )
let G be Function of (REAL-NS n),(REAL-NS n); ( a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of (REAL-NS n) implies ex y being continuous PartFunc of REAL,(REAL-NS n) st
( 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) ) ) )
assume A1:
( a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of (REAL-NS n) )
; ex y being continuous PartFunc of REAL,(REAL-NS n) st
( 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) ) )
then
Fredholm (G,a,b,y0) is with_unique_fixpoint
by Th53;
then consider x being set such that
A2:
( x is_a_fixpoint_of Fredholm (G,a,b,y0) & ( for y being set st y is_a_fixpoint_of Fredholm (G,a,b,y0) holds
x = y ) )
;
A3:
( x in dom (Fredholm (G,a,b,y0)) & x = (Fredholm (G,a,b,y0)) . x )
by A2;
reconsider x = x as Element of the carrier of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))) by A3;
consider f being continuous PartFunc of REAL,(REAL-NS n) such that
A4:
( x = f & dom f = ['a,b'] )
by Def2;
take
f
; ( dom f = ['a,b'] & f is_differentiable_on Z & f /. a = y0 & ( for t being Real st t in Z holds
diff (f,t) = G . (f /. t) ) )
thus
( dom f = ['a,b'] & f is_differentiable_on Z & f /. a = y0 )
by Th54, A4, A1, A3; for t being Real st t in Z holds
diff (f,t) = G . (f /. t)
A5:
].a,b.[ c= [.a,b.]
by XXREAL_1:25;
A6:
['a,b'] = [.a,b.]
by A1, INTEGRA5:def 3;
let t be Real; ( t in Z implies diff (f,t) = G . (f /. t) )
assume A7:
t in Z
; diff (f,t) = G . (f /. t)
dom G = the carrier of (REAL-NS n)
by FUNCT_2:def 1;
then
rng f c= dom G
;
then A8:
dom (G * f) = ['a,b']
by A4, RELAT_1:27;
thus diff (f,t) =
(G * f) /. t
by A7, Th54, A4, A1, A3
.=
(G * f) . t
by A8, A5, A1, A7, A6, PARTFUN1:def 6
.=
G . (f . t)
by A8, A5, A1, A7, A6, FUNCT_1:12
.=
G . (f /. t)
by A5, A1, A7, A6, A4, PARTFUN1:def 6
; verum