let X be RealBanachSpace; :: thesis: for a, b, r being Real
for y0 being VECTOR of X
for G being Function of X,X
for m being Nat 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)) holds ||.(((iter ((Fredholm (G,a,b,y0)),(m + 1))) . u) - ((iter ((Fredholm (G,a,b,y0)),(m + 1))) . v)).|| <= (((r * (b - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).||
let a, b, r be Real; :: thesis: for y0 being VECTOR of X
for G being Function of X,X
for m being Nat 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)) holds ||.(((iter ((Fredholm (G,a,b,y0)),(m + 1))) . u) - ((iter ((Fredholm (G,a,b,y0)),(m + 1))) . v)).|| <= (((r * (b - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).||
let y0 be VECTOR of X; :: thesis: for G being Function of X,X
for m being Nat 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)) holds ||.(((iter ((Fredholm (G,a,b,y0)),(m + 1))) . u) - ((iter ((Fredholm (G,a,b,y0)),(m + 1))) . v)).|| <= (((r * (b - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).||
let G be Function of X,X; :: thesis: for m being Nat 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)) holds ||.(((iter ((Fredholm (G,a,b,y0)),(m + 1))) . u) - ((iter ((Fredholm (G,a,b,y0)),(m + 1))) . v)).|| <= (((r * (b - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).||
let m be Nat; :: thesis: ( a <= b & 0 < r & ( for y1, y2 being VECTOR of X holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) implies for u, v being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) holds ||.(((iter ((Fredholm (G,a,b,y0)),(m + 1))) . u) - ((iter ((Fredholm (G,a,b,y0)),(m + 1))) . v)).|| <= (((r * (b - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).|| )
assume A1: ( a <= b & 0 < r & ( for y1, y2 being VECTOR of X holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) ) ; :: thesis: for u, v being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) holds ||.(((iter ((Fredholm (G,a,b,y0)),(m + 1))) . u) - ((iter ((Fredholm (G,a,b,y0)),(m + 1))) . v)).|| <= (((r * (b - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).||
let u, v be VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)); :: thesis: ||.(((iter ((Fredholm (G,a,b,y0)),(m + 1))) . u) - ((iter ((Fredholm (G,a,b,y0)),(m + 1))) . v)).|| <= (((r * (b - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).||
reconsider u1 = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . u as VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) ;
reconsider v1 = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . v as VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) ;
consider g being continuous PartFunc of REAL, the carrier of X such that
A2: ( u1 = g & dom g = ['a,b'] ) by ORDEQ_01:def 2;
consider h being continuous PartFunc of REAL, the carrier of X such that
A3: ( v1 = h & dom h = ['a,b'] ) by ORDEQ_01:def 2;

now :: thesis: for t being Real st t in ['a,b'] holds
||.((g /. t) - (h /. t)).|| <= (((r * (b - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).||

let t be Real; :: thesis: ( t in ['a,b'] implies ||.((g /. t) - (h /. t)).|| <= (((r * (b - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).|| )
A4: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
assume A5: t in ['a,b'] ; :: thesis: ||.((g /. t) - (h /. t)).|| <= (((r * (b - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).||
then A6: ex g being Real st
( t = g & a <= g & g <= b ) by A4;
m in NAT by ORDINAL1:def 12;
then A7: ||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).|| by A5, Th54, A1, A2, A3;
(((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).|| <= (((r * (b - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).|| by A6, A1, Lm8;
hence ||.((g /. t) - (h /. t)).|| <= (((r * (b - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).|| by A7, XXREAL_0:2; :: thesis: verum

end;

hence ||.(((iter ((Fredholm (G,a,b,y0)),(m + 1))) . u) - ((iter ((Fredholm (G,a,b,y0)),(m + 1))) . v)).|| <= (((r * (b - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).|| by ORDEQ_01:27, A2, A3; :: thesis: verum