theorem Th54: :: ORDEQ_02:23

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 m being Element of NAT
for g, h being continuous PartFunc of REAL, the carrier of X st g = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . u & h = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . v holds
for t being Real st t in ['a,b'] holds
||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).||