let n be non zero Element of NAT ; :: thesis: 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) 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)))
for g, h being continuous PartFunc of REAL,(REAL-NS n) st g = (Fredholm (G,a,b,y0)) . u & h = (Fredholm (G,a,b,y0)) . v holds
for t being Real st t in ['a,b'] holds
||.((g /. t) - (h /. t)).|| <= (r * (t - a)) * ||.(u - v).||
let a, b, r 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 & 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)))
for g, h being continuous PartFunc of REAL,(REAL-NS n) st g = (Fredholm (G,a,b,y0)) . u & h = (Fredholm (G,a,b,y0)) . v holds
for t being Real st t in ['a,b'] holds
||.((g /. t) - (h /. t)).|| <= (r * (t - a)) * ||.(u - v).||
let y0 be VECTOR of (REAL-NS n); :: thesis: for G being Function of (REAL-NS n),(REAL-NS n) 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)))
for g, h being continuous PartFunc of REAL,(REAL-NS n) st g = (Fredholm (G,a,b,y0)) . u & h = (Fredholm (G,a,b,y0)) . v holds
for t being Real st t in ['a,b'] holds
||.((g /. t) - (h /. t)).|| <= (r * (t - a)) * ||.(u - v).||
let G be Function of (REAL-NS n),(REAL-NS n); :: thesis: ( 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)))
for g, h being continuous PartFunc of REAL,(REAL-NS n) st g = (Fredholm (G,a,b,y0)) . u & h = (Fredholm (G,a,b,y0)) . v holds
for t being Real st t in ['a,b'] holds
||.((g /. t) - (h /. t)).|| <= (r * (t - a)) * ||.(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).|| ) ) ; :: thesis: for u, v being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n)))
for g, h being continuous PartFunc of REAL,(REAL-NS n) st g = (Fredholm (G,a,b,y0)) . u & h = (Fredholm (G,a,b,y0)) . v holds
for t being Real st t in ['a,b'] holds
||.((g /. t) - (h /. t)).|| <= (r * (t - a)) * ||.(u - v).||
A2: dom G = the carrier of (REAL-NS n) by FUNCT_2:def 1;
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 A1;
then G is_Lipschitzian_on the carrier of (REAL-NS n) by A1, A2, NFCONT_1:def 9;
then A3: G is_continuous_on dom G by A2, NFCONT_1:45;
let u, v be VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))); :: thesis: for g, h being continuous PartFunc of REAL,(REAL-NS n) st g = (Fredholm (G,a,b,y0)) . u & h = (Fredholm (G,a,b,y0)) . v holds
for t being Real st t in ['a,b'] holds
||.((g /. t) - (h /. t)).|| <= (r * (t - a)) * ||.(u - v).||
let g, h be continuous PartFunc of REAL,(REAL-NS n); :: thesis: ( g = (Fredholm (G,a,b,y0)) . u & h = (Fredholm (G,a,b,y0)) . v implies for t being Real st t in ['a,b'] holds
||.((g /. t) - (h /. t)).|| <= (r * (t - a)) * ||.(u - v).|| )
assume A4: ( g = (Fredholm (G,a,b,y0)) . u & h = (Fredholm (G,a,b,y0)) . v ) ; :: thesis: for t being Real st t in ['a,b'] holds
||.((g /. t) - (h /. t)).|| <= (r * (t - a)) * ||.(u - v).||
set F = Fredholm (G,a,b,y0);
consider f1, g1, Gf1 being continuous PartFunc of REAL,(REAL-NS n) such that
A5: ( u = f1 & (Fredholm (G,a,b,y0)) . u = g1 & dom f1 = ['a,b'] & dom g1 = ['a,b'] & Gf1 = G * f1 & ( for t being Real st t in ['a,b'] holds
g1 . t = y0 + (integral (Gf1,a,t)) ) ) by Def7, A1, A3;
consider f2, g2, Gf2 being continuous PartFunc of REAL,(REAL-NS n) such that
A6: ( v = f2 & (Fredholm (G,a,b,y0)) . v = g2 & dom f2 = ['a,b'] & dom g2 = ['a,b'] & Gf2 = G * f2 & ( for t being Real st t in ['a,b'] holds
g2 . t = y0 + (integral (Gf2,a,t)) ) ) by Def7, A1, A3;
set Gf12 = Gf1 - Gf2;
A7: dom G = the carrier of (REAL-NS n) by FUNCT_2:def 1;
then rng f1 c= dom G ;
then A8: dom Gf1 = ['a,b'] by A5, RELAT_1:27;
rng f2 c= dom G by A7;
then A9: dom Gf2 = ['a,b'] by A6, RELAT_1:27;
reconsider Gf12 = Gf1 - Gf2 as continuous PartFunc of REAL,(REAL-NS n) ;
A10: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
let t be Real; :: thesis: ( t in ['a,b'] implies ||.((g /. t) - (h /. t)).|| <= (r * (t - a)) * ||.(u - v).|| )
assume A11: t in ['a,b'] ; :: thesis: ||.((g /. t) - (h /. t)).|| <= (r * (t - a)) * ||.(u - v).||
then A12: ex g being Real st
( t = g & a <= g & g <= b ) by A10;
A13: dom Gf12 = (dom Gf1) /\ (dom Gf2) by VFUNCT_1:def 2
.= ['a,b'] by A8, A9 ;
A14: Gf12 is_integrable_on ['a,b'] by A13, Th33;
A15: Gf12 | ['a,b'] is bounded by A13, Th32;
Gf12 | ['a,b'] is continuous ;
then A16: ||.Gf12.|| | ['a,b'] is continuous by A13, NFCONT_3:22;
['a,b'] = dom ||.Gf12.|| by A13, NORMSP_0:def 2;
then A17: ||.Gf12.|| is_integrable_on ['a,b'] by A16, INTEGRA5:11;
A18: a in ['a,b'] by A10, A1;
for x being Real st x in ['a,t'] holds
||.(Gf12 /. x).|| <= r * ||.(u - v).||

proof

let x be Real; :: thesis: ( x in ['a,t'] implies ||.(Gf12 /. x).|| <= r * ||.(u - v).|| )
assume A19: x in ['a,t'] ; :: thesis: ||.(Gf12 /. x).|| <= r * ||.(u - v).||
A20: ['a,t'] c= ['a,b'] by A12, INTEGR19:1;
A21: Gf12 /. x = (Gf1 /. x) - (Gf2 /. x) by A13, A20, A19, VFUNCT_1:def 2;
A22: Gf1 /. x = Gf1 . x by A8, A20, A19, PARTFUN1:def 6
.= G . (f1 . x) by A20, A19, A8, A5, FUNCT_1:12
.= G /. (f1 /. x) by A20, A19, A5, PARTFUN1:def 6 ;
A23: Gf2 /. x = Gf2 . x by A9, A20, A19, PARTFUN1:def 6
.= G . (f2 . x) by A20, A19, A9, A6, FUNCT_1:12
.= G /. (f2 /. x) by A20, A19, A6, PARTFUN1:def 6 ;
A24: ||.((Gf1 /. x) - (Gf2 /. x)).|| <= r * ||.((f1 /. x) - (f2 /. x)).|| by A22, A23, A1;
||.((f1 /. x) - (f2 /. x)).|| <= ||.(u - v).|| by A20, A19, A5, A6, Th26;
then r * ||.((f1 /. x) - (f2 /. x)).|| <= r * ||.(u - v).|| by A1, XREAL_1:64;
hence ||.(Gf12 /. x).|| <= r * ||.(u - v).|| by A21, A24, XXREAL_0:2; :: thesis: verum

end;

then A25: ||.(integral (Gf12,a,t)).|| <= (r * ||.(u - v).||) * (t - a) by Th45, A1, A17, A14, A15, A13, A18, A11, A12;
A26: Gf1 is_integrable_on ['a,b'] by A8, Th33;
A27: Gf1 | ['a,b'] is bounded by A8, Th32;
A28: Gf2 is_integrable_on ['a,b'] by A9, Th33;
A29: Gf2 | ['a,b'] is bounded by A9, Th32;
A30: integral (Gf12,a,t) = (integral (Gf1,a,t)) - (integral (Gf2,a,t)) by A8, A9, A26, A27, A28, A29, A18, A11, A1, INTEGR19:50;
A31: g /. t = g1 . t by A4, A11, A5, PARTFUN1:def 6
.= y0 + (integral (Gf1,a,t)) by A5, A11 ;
A32: h /. t = g2 . t by A4, A11, A6, PARTFUN1:def 6
.= y0 + (integral (Gf2,a,t)) by A6, A11 ;
(g /. t) - (h /. t) = ((y0 + (integral (Gf1,a,t))) - y0) - (integral (Gf2,a,t)) by A31, A32, RLVECT_1:27
.= ((integral (Gf1,a,t)) + (y0 - y0)) - (integral (Gf2,a,t)) by RLVECT_1:28
.= ((integral (Gf1,a,t)) + (0. (REAL-NS n))) - (integral (Gf2,a,t)) by RLVECT_1:15
.= integral (Gf12,a,t) by A30 ;
hence ||.((g /. t) - (h /. t)).|| <= (r * (t - a)) * ||.(u - v).|| by A25; :: thesis: verum