theorem Th59: :: ORDEQ_02:28

for X being 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)