let n be non zero Element of NAT ; 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; 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); 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); ( 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) )
; 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
; 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; verum