let n be non zero Element of NAT ; :: thesis: for a, b being Real
for y0 being VECTOR of (REAL-NS n)
for G being Function of (REAL-NS n),(REAL-NS n) st a < b & G is_Lipschitzian_on the carrier of (REAL-NS n) 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 (REAL-NS n)
for G being Function of (REAL-NS n),(REAL-NS n) st a < b & G is_Lipschitzian_on the carrier of (REAL-NS n) holds
ex m being Nat st iter ((Fredholm (G,a,b,y0)),(m + 1)) is contraction
let y0 be VECTOR of (REAL-NS n); :: thesis: for G being Function of (REAL-NS n),(REAL-NS n) st a < b & G is_Lipschitzian_on the carrier of (REAL-NS n) holds
ex m being Nat st iter ((Fredholm (G,a,b,y0)),(m + 1)) is contraction
let G be Function of (REAL-NS n),(REAL-NS n); :: thesis: ( a < b & G is_Lipschitzian_on the carrier of (REAL-NS n) 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 (REAL-NS n) ) ; :: 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 (REAL-NS n) st x1 in the carrier of (REAL-NS n) & x2 in the carrier of (REAL-NS n) holds
||.((G /. x1) - (G /. x2)).|| <= r * ||.(x1 - x2).|| ) ) by NFCONT_1:def 9;
A3: for x1, x2 being Point of (REAL-NS n) 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 Lm14, 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'],(REAL-NS n))) 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 Th51, A3, A2, A1;
hence iter ((Fredholm (G,a,b,y0)),(m + 1)) is contraction by A4; :: thesis: verum