let X be RealBanachSpace; :: thesis: for a, b, r being Real

for y0 being VECTOR of X

for G being Function of X,X st a <= b & 0 < r & ( for y1, y2 being VECTOR of X holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) holds

for u, v being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X))

for g, h being continuous PartFunc of REAL, the carrier of X 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 X

for G being Function of X,X st a <= b & 0 < r & ( for y1, y2 being VECTOR of X holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) holds

for u, v being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X))

for g, h being continuous PartFunc of REAL, the carrier of X 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 X; :: thesis: for G being Function of X,X st a <= b & 0 < r & ( for y1, y2 being VECTOR of X holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) holds

for u, v being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X))

for g, h being continuous PartFunc of REAL, the carrier of X 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 X,X; :: thesis: ( a <= b & 0 < r & ( for y1, y2 being VECTOR of X holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) implies for u, v being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X))

for g, h being continuous PartFunc of REAL, the carrier of X 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 X holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) ) ; :: thesis: for u, v being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X))

for g, h being continuous PartFunc of REAL, the carrier of X 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 X by FUNCT_2:def 1;

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).|| by A1;

then G is_Lipschitzian_on the carrier of X by A1, FUNCT_2:def 1;

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'],X)); :: thesis: for g, h being continuous PartFunc of REAL, the carrier of X 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, the carrier of X; :: 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, the carrier of X 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 Def8, A1, A3;

consider f2, g2, Gf2 being continuous PartFunc of REAL, the carrier of X 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 Def8, A1, A3;

set Gf12 = Gf1 - Gf2;

dom G = the carrier of X by FUNCT_2:def 1;

then ( rng f1 c= dom G & rng f2 c= dom G ) ;

then A8: ( dom Gf1 = ['a,b'] & dom Gf2 = ['a,b'] ) by A5, A6, RELAT_1:27;

reconsider Gf12 = Gf1 - Gf2 as continuous PartFunc of REAL, the carrier of X ;

A10: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;

then A18: a in ['a,b'] by A1;

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;

then A20: ['a,t'] c= ['a,b'] by INTEGR19:1;

X1: ['a,t'] = [.a,t.] by A12, INTEGRA5:def 3;

A13: dom Gf12 = (dom Gf1) /\ (dom Gf2) by VFUNCT_1:def 2;

for x being Real st x in ['a,t'] holds

||.(Gf12 /. x).|| <= r * ||.(u - v).||

( g /. t = y0 + (integral (Gf1,a,t)) & h /. t = y0 + (integral (Gf2,a,t)) ) by A4, A5, A6, A11;

then (g /. t) - (h /. t) = ((y0 + (integral (Gf1,a,t))) - y0) - (integral (Gf2,a,t)) by RLVECT_1:27

.= ((integral (Gf1,a,t)) + (y0 - y0)) - (integral (Gf2,a,t)) by RLVECT_1:28

.= ((integral (Gf1,a,t)) + (0. X)) - (integral (Gf2,a,t)) by RLVECT_1:15

.= integral (Gf12,a,t) by A8, A18, A11, A1, INTEGR21:30 ;

hence ||.((g /. t) - (h /. t)).|| <= (r * (t - a)) * ||.(u - v).|| by A25; :: thesis: verum

for y0 being VECTOR of X

for G being Function of X,X st a <= b & 0 < r & ( for y1, y2 being VECTOR of X holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) holds

for u, v being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X))

for g, h being continuous PartFunc of REAL, the carrier of X 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 X

for G being Function of X,X st a <= b & 0 < r & ( for y1, y2 being VECTOR of X holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) holds

for u, v being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X))

for g, h being continuous PartFunc of REAL, the carrier of X 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 X; :: thesis: for G being Function of X,X st a <= b & 0 < r & ( for y1, y2 being VECTOR of X holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) holds

for u, v being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X))

for g, h being continuous PartFunc of REAL, the carrier of X 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 X,X; :: thesis: ( a <= b & 0 < r & ( for y1, y2 being VECTOR of X holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) implies for u, v being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X))

for g, h being continuous PartFunc of REAL, the carrier of X 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 X holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) ) ; :: thesis: for u, v being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X))

for g, h being continuous PartFunc of REAL, the carrier of X 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 X by FUNCT_2:def 1;

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).|| by A1;

then G is_Lipschitzian_on the carrier of X by A1, FUNCT_2:def 1;

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'],X)); :: thesis: for g, h being continuous PartFunc of REAL, the carrier of X 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, the carrier of X; :: 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, the carrier of X 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 Def8, A1, A3;

consider f2, g2, Gf2 being continuous PartFunc of REAL, the carrier of X 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 Def8, A1, A3;

set Gf12 = Gf1 - Gf2;

dom G = the carrier of X by FUNCT_2:def 1;

then ( rng f1 c= dom G & rng f2 c= dom G ) ;

then A8: ( dom Gf1 = ['a,b'] & dom Gf2 = ['a,b'] ) by A5, A6, RELAT_1:27;

reconsider Gf12 = Gf1 - Gf2 as continuous PartFunc of REAL, the carrier of X ;

A10: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;

then A18: a in ['a,b'] by A1;

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;

then A20: ['a,t'] c= ['a,b'] by INTEGR19:1;

X1: ['a,t'] = [.a,t.] by A12, INTEGRA5:def 3;

A13: dom Gf12 = (dom Gf1) /\ (dom Gf2) by VFUNCT_1:def 2;

for x being Real st x in ['a,t'] holds

||.(Gf12 /. x).|| <= r * ||.(u - v).||

proof

then A25:
||.(integral (Gf12,a,t)).|| <= (r * ||.(u - v).||) * (t - a)
by Lm14a, X1, A8, A13, A18, A10, A11, A12;
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).||

then A21: Gf12 /. x = (Gf1 /. x) - (Gf2 /. x) by A8, A13, A20, VFUNCT_1:def 2;

A24: r * ||.((f1 /. x) - (f2 /. x)).|| <= r * ||.(u - v).|| by A1, XREAL_1:64, A19, A20, A5, A6, ORDEQ_01:26;

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 ;

Gf2 /. x = Gf2 . x by A8, A20, A19, PARTFUN1:def 6

.= G . (f2 . x) by A20, A19, A8, A6, FUNCT_1:12

.= G /. (f2 /. x) by A20, A19, A6, PARTFUN1:def 6 ;

then ||.((Gf1 /. x) - (Gf2 /. x)).|| <= r * ||.((f1 /. x) - (f2 /. x)).|| by A22, A1;

hence ||.(Gf12 /. x).|| <= r * ||.(u - v).|| by A21, A24, XXREAL_0:2; :: thesis: verum

end;assume A19: x in ['a,t'] ; :: thesis: ||.(Gf12 /. x).|| <= r * ||.(u - v).||

then A21: Gf12 /. x = (Gf1 /. x) - (Gf2 /. x) by A8, A13, A20, VFUNCT_1:def 2;

A24: r * ||.((f1 /. x) - (f2 /. x)).|| <= r * ||.(u - v).|| by A1, XREAL_1:64, A19, A20, A5, A6, ORDEQ_01:26;

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 ;

Gf2 /. x = Gf2 . x by A8, A20, A19, PARTFUN1:def 6

.= G . (f2 . x) by A20, A19, A8, A6, FUNCT_1:12

.= G /. (f2 /. x) by A20, A19, A6, PARTFUN1:def 6 ;

then ||.((Gf1 /. x) - (Gf2 /. x)).|| <= r * ||.((f1 /. x) - (f2 /. x)).|| by A22, A1;

hence ||.(Gf12 /. x).|| <= r * ||.(u - v).|| by A21, A24, XXREAL_0:2; :: thesis: verum

( g /. t = y0 + (integral (Gf1,a,t)) & h /. t = y0 + (integral (Gf2,a,t)) ) by A4, A5, A6, A11;

then (g /. t) - (h /. t) = ((y0 + (integral (Gf1,a,t))) - y0) - (integral (Gf2,a,t)) by RLVECT_1:27

.= ((integral (Gf1,a,t)) + (y0 - y0)) - (integral (Gf2,a,t)) by RLVECT_1:28

.= ((integral (Gf1,a,t)) + (0. X)) - (integral (Gf2,a,t)) by RLVECT_1:15

.= integral (Gf12,a,t) by A8, A18, A11, A1, INTEGR21:30 ;

hence ||.((g /. t) - (h /. t)).|| <= (r * (t - a)) * ||.(u - v).|| by A25; :: thesis: verum