let X be RealBanachSpace; 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; 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; 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; ( 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 )
; 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
; 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; verum