let n be non zero Element of NAT ; for a, b, r being Real
for y0 being VECTOR of (REAL-NS n)
for G being Function of (REAL-NS n),(REAL-NS n)
for m being Nat st a <= b & 0 < r & ( for y1, y2 being VECTOR of (REAL-NS n) holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) holds
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).||
let a, b, r be Real; for y0 being VECTOR of (REAL-NS n)
for G being Function of (REAL-NS n),(REAL-NS n)
for m being Nat st a <= b & 0 < r & ( for y1, y2 being VECTOR of (REAL-NS n) holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) holds
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).||
let y0 be VECTOR of (REAL-NS n); for G being Function of (REAL-NS n),(REAL-NS n)
for m being Nat st a <= b & 0 < r & ( for y1, y2 being VECTOR of (REAL-NS n) holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) holds
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).||
let G be Function of (REAL-NS n),(REAL-NS n); for m being Nat st a <= b & 0 < r & ( for y1, y2 being VECTOR of (REAL-NS n) holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) holds
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).||
let m be Nat; ( a <= b & 0 < r & ( for y1, y2 being VECTOR of (REAL-NS n) holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) implies 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).|| )
assume A1:
( a <= b & 0 < r & ( for y1, y2 being VECTOR of (REAL-NS n) holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) )
; 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).||
let u, v be VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))); ||.(((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).||
reconsider u1 = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . u as VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))) ;
reconsider v1 = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . v as VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))) ;
consider g being continuous PartFunc of REAL,(REAL-NS n) such that
A2:
( u1 = g & dom g = ['a,b'] )
by Def2;
consider h being continuous PartFunc of REAL,(REAL-NS n) such that
A3:
( v1 = h & dom h = ['a,b'] )
by Def2;
now for t being Real st t in ['a,b'] holds
||.((g /. t) - (h /. t)).|| <= (((r * (b - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).||let t be
Real;
( t in ['a,b'] implies ||.((g /. t) - (h /. t)).|| <= (((r * (b - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).|| )A4:
['a,b'] = [.a,b.]
by A1, INTEGRA5:def 3;
assume A5:
t in ['a,b']
;
||.((g /. t) - (h /. t)).|| <= (((r * (b - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).||then A6:
ex
g being
Real st
(
t = g &
a <= g &
g <= b )
by A4;
m in NAT
by ORDINAL1:def 12;
then A7:
||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).||
by A5, Th50, A1, A2, A3;
(((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).|| <= (((r * (b - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).||
by A6, A1, Lm13;
hence
||.((g /. t) - (h /. t)).|| <= (((r * (b - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).||
by A7, XXREAL_0:2;
verum end;
hence
||.(((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 Th27, A2, A3; verum