theorem Th56: :: ORDEQ_02:25

for X being RealBanachSpace
for a, b being Real
for y0 being VECTOR of X
for G being Function of X,X st a < b & G is_Lipschitzian_on the carrier of X holds
ex m being Nat st iter ((Fredholm (G,a,b,y0)),(m + 1)) is contraction