let X be RealBanachSpace; :: thesis: 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

let a, b be Real; :: thesis: 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

let y0 be VECTOR of X; :: thesis: 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

let G be Function of X,X; :: thesis: ( a < b & G is_Lipschitzian_on the carrier of X implies ex m being Nat st iter ((Fredholm (G,a,b,y0)),(m + 1)) is contraction )

assume A1: ( a < b & G is_Lipschitzian_on the carrier of X ) ; :: thesis: ex m being Nat st iter ((Fredholm (G,a,b,y0)),(m + 1)) is contraction

then consider r being Real such that

A2: ( 0 < r & ( for x1, x2 being Point of X st x1 in the carrier of X & x2 in the carrier of X holds

||.((G /. x1) - (G /. x2)).|| <= r * ||.(x1 - x2).|| ) ) ;

A3: for x1, x2 being Point of X holds ||.((G /. x1) - (G /. x2)).|| <= r * ||.(x1 - x2).|| by A2;

consider m being Element of NAT such that

A4: ( ((r * (b - a)) |^ (m + 1)) / ((m + 1) !) < 1 & 0 < ((r * (b - a)) |^ (m + 1)) / ((m + 1) !) ) by Lm9, A1, A2;

take m ; :: thesis: iter ((Fredholm (G,a,b,y0)),(m + 1)) is contraction

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).|| by Th55, A3, A2, A1;

hence iter ((Fredholm (G,a,b,y0)),(m + 1)) is contraction by A4; :: thesis: verum

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

let a, b be Real; :: thesis: 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

let y0 be VECTOR of X; :: thesis: 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

let G be Function of X,X; :: thesis: ( a < b & G is_Lipschitzian_on the carrier of X implies ex m being Nat st iter ((Fredholm (G,a,b,y0)),(m + 1)) is contraction )

assume A1: ( a < b & G is_Lipschitzian_on the carrier of X ) ; :: thesis: ex m being Nat st iter ((Fredholm (G,a,b,y0)),(m + 1)) is contraction

then consider r being Real such that

A2: ( 0 < r & ( for x1, x2 being Point of X st x1 in the carrier of X & x2 in the carrier of X holds

||.((G /. x1) - (G /. x2)).|| <= r * ||.(x1 - x2).|| ) ) ;

A3: for x1, x2 being Point of X holds ||.((G /. x1) - (G /. x2)).|| <= r * ||.(x1 - x2).|| by A2;

consider m being Element of NAT such that

A4: ( ((r * (b - a)) |^ (m + 1)) / ((m + 1) !) < 1 & 0 < ((r * (b - a)) |^ (m + 1)) / ((m + 1) !) ) by Lm9, A1, A2;

take m ; :: thesis: iter ((Fredholm (G,a,b,y0)),(m + 1)) is contraction

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).|| by Th55, A3, A2, A1;

hence iter ((Fredholm (G,a,b,y0)),(m + 1)) is contraction by A4; :: thesis: verum