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