theorem Th53: :: ORDEQ_02:22

for X being RealBanachSpace
for a, b, r being Real
for y0 being VECTOR of X
for G being Function of X,X st a <= b & 0 < r & ( for y1, y2 being VECTOR of X holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) holds
for u, v being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X))
for g, h being continuous PartFunc of REAL, the carrier of X st g = (Fredholm (G,a,b,y0)) . u & h = (Fredholm (G,a,b,y0)) . v holds
for t being Real st t in ['a,b'] holds
||.((g /. t) - (h /. t)).|| <= (r * (t - a)) * ||.(u - v).||