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;

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).||

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||.((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;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