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 m being Element of NAT

for g, h being continuous PartFunc of REAL, the carrier of X st g = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . u & h = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . v holds

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

||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(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 m being Element of NAT

for g, h being continuous PartFunc of REAL, the carrier of X st g = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . u & h = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . v holds

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

||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(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 m being Element of NAT

for g, h being continuous PartFunc of REAL, the carrier of X st g = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . u & h = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . v holds

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

||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(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 m being Element of NAT

for g, h being continuous PartFunc of REAL, the carrier of X st g = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . u & h = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . v holds

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

||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(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 m being Element of NAT

for g, h being continuous PartFunc of REAL, the carrier of X st g = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . u & h = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . v holds

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

||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).||

set F = Fredholm (G,a,b,y0);

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 u1, v1 be VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)); :: thesis: for m being Element of NAT

for g, h being continuous PartFunc of REAL, the carrier of X st g = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . u1 & h = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . v1 holds

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

||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u1 - v1).||

defpred S_{1}[ Nat] means for g, h being continuous PartFunc of REAL, the carrier of X st g = (iter ((Fredholm (G,a,b,y0)),($1 + 1))) . u1 & h = (iter ((Fredholm (G,a,b,y0)),($1 + 1))) . v1 holds

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

||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ ($1 + 1)) / (($1 + 1) !)) * ||.(u1 - v1).||;

reconsider Z0 = 0 as Element of NAT ;

A4: S_{1}[ 0 ]
_{1}[k] holds

S_{1}[k + 1]
_{1}[k]
from NAT_1:sch 2(A4, A8);

hence for m being Element of NAT

for g, h being continuous PartFunc of REAL, the carrier of X st g = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . u1 & h = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . v1 holds

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

||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u1 - v1).|| ; :: 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 m being Element of NAT

for g, h being continuous PartFunc of REAL, the carrier of X st g = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . u & h = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . v holds

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

||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(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 m being Element of NAT

for g, h being continuous PartFunc of REAL, the carrier of X st g = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . u & h = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . v holds

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

||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(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 m being Element of NAT

for g, h being continuous PartFunc of REAL, the carrier of X st g = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . u & h = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . v holds

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

||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(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 m being Element of NAT

for g, h being continuous PartFunc of REAL, the carrier of X st g = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . u & h = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . v holds

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

||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(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 m being Element of NAT

for g, h being continuous PartFunc of REAL, the carrier of X st g = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . u & h = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . v holds

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

||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).||

set F = Fredholm (G,a,b,y0);

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 u1, v1 be VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)); :: thesis: for m being Element of NAT

for g, h being continuous PartFunc of REAL, the carrier of X st g = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . u1 & h = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . v1 holds

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

||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u1 - v1).||

defpred S

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

||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ ($1 + 1)) / (($1 + 1) !)) * ||.(u1 - v1).||;

reconsider Z0 = 0 as Element of NAT ;

A4: S

proof

A8:
for k being Nat st S
let g, h be continuous PartFunc of REAL, the carrier of X; :: thesis: ( g = (iter ((Fredholm (G,a,b,y0)),(0 + 1))) . u1 & h = (iter ((Fredholm (G,a,b,y0)),(0 + 1))) . v1 implies for t being Real st t in ['a,b'] holds

||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (0 + 1)) / ((0 + 1) !)) * ||.(u1 - v1).|| )

assume ( g = (iter ((Fredholm (G,a,b,y0)),(0 + 1))) . u1 & h = (iter ((Fredholm (G,a,b,y0)),(0 + 1))) . v1 ) ; :: thesis: for t being Real st t in ['a,b'] holds

||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (0 + 1)) / ((0 + 1) !)) * ||.(u1 - v1).||

then A6: ( g = (Fredholm (G,a,b,y0)) . u1 & h = (Fredholm (G,a,b,y0)) . v1 ) by FUNCT_7:70;

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

||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (Z0 + 1)) / ((Z0 + 1) !)) * ||.(u1 - v1).|| by NEWTON:13, Th53, A1, A6;

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

||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (0 + 1)) / ((0 + 1) !)) * ||.(u1 - v1).|| ; :: thesis: verum

end;||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (0 + 1)) / ((0 + 1) !)) * ||.(u1 - v1).|| )

assume ( g = (iter ((Fredholm (G,a,b,y0)),(0 + 1))) . u1 & h = (iter ((Fredholm (G,a,b,y0)),(0 + 1))) . v1 ) ; :: thesis: for t being Real st t in ['a,b'] holds

||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (0 + 1)) / ((0 + 1) !)) * ||.(u1 - v1).||

then A6: ( g = (Fredholm (G,a,b,y0)) . u1 & h = (Fredholm (G,a,b,y0)) . v1 ) by FUNCT_7:70;

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

||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (Z0 + 1)) / ((Z0 + 1) !)) * ||.(u1 - v1).|| by NEWTON:13, Th53, A1, A6;

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

||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (0 + 1)) / ((0 + 1) !)) * ||.(u1 - v1).|| ; :: thesis: verum

S

proof

for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A9: S_{1}[k]
; :: thesis: S_{1}[k + 1]

let g, h be continuous PartFunc of REAL, the carrier of X; :: thesis: ( g = (iter ((Fredholm (G,a,b,y0)),((k + 1) + 1))) . u1 & h = (iter ((Fredholm (G,a,b,y0)),((k + 1) + 1))) . v1 implies for t being Real st t in ['a,b'] holds

||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ ((k + 1) + 1)) / (((k + 1) + 1) !)) * ||.(u1 - v1).|| )

assume A10: ( g = (iter ((Fredholm (G,a,b,y0)),((k + 1) + 1))) . u1 & h = (iter ((Fredholm (G,a,b,y0)),((k + 1) + 1))) . v1 ) ; :: thesis: for t being Real st t in ['a,b'] holds

||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ ((k + 1) + 1)) / (((k + 1) + 1) !)) * ||.(u1 - v1).||

reconsider u = (iter ((Fredholm (G,a,b,y0)),(k + 1))) . u1, v = (iter ((Fredholm (G,a,b,y0)),(k + 1))) . v1 as VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) ;

A11: dom (iter ((Fredholm (G,a,b,y0)),(k + 1))) = the carrier of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) by FUNCT_2:def 1;

A12: (iter ((Fredholm (G,a,b,y0)),((k + 1) + 1))) . u1 = ((Fredholm (G,a,b,y0)) * (iter ((Fredholm (G,a,b,y0)),(k + 1)))) . u1 by FUNCT_7:71

.= (Fredholm (G,a,b,y0)) . u by A11, FUNCT_1:13 ;

A13: (iter ((Fredholm (G,a,b,y0)),((k + 1) + 1))) . v1 = ((Fredholm (G,a,b,y0)) * (iter ((Fredholm (G,a,b,y0)),(k + 1)))) . v1 by FUNCT_7:71

.= (Fredholm (G,a,b,y0)) . v by A11, FUNCT_1:13 ;

consider f1, g1, Gf1 being continuous PartFunc of REAL, the carrier of X such that

A14: ( 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

A15: ( 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 A18: ( dom Gf1 = ['a,b'] & dom Gf2 = ['a,b'] ) by A14, A15, RELAT_1:27;

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

A20: ['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)) |^ ((k + 1) + 1)) / (((k + 1) + 1) !)) * ||.(u1 - v1).|| )

assume A21: t in ['a,b'] ; :: thesis: ||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ ((k + 1) + 1)) / (((k + 1) + 1) !)) * ||.(u1 - v1).||

then A22: ex g being Real st

( t = g & a <= g & g <= b ) by A20;

a22: ex g being Element of REAL st

( t = g & a <= g & g <= b )

.= ['a,b'] by A18 ;

then A24: dom ||.Gf12.|| = ['a,b'] by NORMSP_0:def 2;

A27: a in ['a,b'] by A20, A1;

( min (a,t) = a & max (a,t) = t ) by A22, XXREAL_0:def 9, XXREAL_0:def 10;

then A30: ( ||.Gf12.|| is_integrable_on ['a,t'] & ||.Gf12.|| | ['a,t'] is bounded & ||.(integral (Gf12,a,t)).|| <= integral (||.Gf12.||,a,t) ) by A1, A23, A27, A21, INTEGR21:22;

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

then consider rg being PartFunc of REAL,REAL such that

A31: ( dom rg = ['a,t'] & ( for x being Real st x in ['a,t'] holds

rg . x = r * ((((r * (x - a)) |^ (k + 1)) / ((k + 1) !)) * ||.(u1 - v1).||) ) & rg is continuous & rg is_integrable_on ['a,t'] & rg | ['a,t'] is bounded & integral (rg,a,t) = (((r * (t - a)) |^ ((k + 1) + 1)) / (((k + 1) + 1) !)) * ||.(u1 - v1).|| ) by Lm7, a22;

A32: ['a,t'] c= ['a,b'] by A22, INTEGR19:1;

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

||.Gf12.|| . x <= rg . x

( g /. t = y0 + (integral (Gf1,a,t)) & h /. t = y0 + (integral (Gf2,a,t)) ) by A14, A15, A21, A12, A10, A13;

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 A18, A27, A21, A1, INTEGR21:30 ;

hence ||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ ((k + 1) + 1)) / (((k + 1) + 1) !)) * ||.(u1 - v1).|| by A38, A30, XXREAL_0:2, A31; :: thesis: verum

end;assume A9: S

let g, h be continuous PartFunc of REAL, the carrier of X; :: thesis: ( g = (iter ((Fredholm (G,a,b,y0)),((k + 1) + 1))) . u1 & h = (iter ((Fredholm (G,a,b,y0)),((k + 1) + 1))) . v1 implies for t being Real st t in ['a,b'] holds

||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ ((k + 1) + 1)) / (((k + 1) + 1) !)) * ||.(u1 - v1).|| )

assume A10: ( g = (iter ((Fredholm (G,a,b,y0)),((k + 1) + 1))) . u1 & h = (iter ((Fredholm (G,a,b,y0)),((k + 1) + 1))) . v1 ) ; :: thesis: for t being Real st t in ['a,b'] holds

||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ ((k + 1) + 1)) / (((k + 1) + 1) !)) * ||.(u1 - v1).||

reconsider u = (iter ((Fredholm (G,a,b,y0)),(k + 1))) . u1, v = (iter ((Fredholm (G,a,b,y0)),(k + 1))) . v1 as VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) ;

A11: dom (iter ((Fredholm (G,a,b,y0)),(k + 1))) = the carrier of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) by FUNCT_2:def 1;

A12: (iter ((Fredholm (G,a,b,y0)),((k + 1) + 1))) . u1 = ((Fredholm (G,a,b,y0)) * (iter ((Fredholm (G,a,b,y0)),(k + 1)))) . u1 by FUNCT_7:71

.= (Fredholm (G,a,b,y0)) . u by A11, FUNCT_1:13 ;

A13: (iter ((Fredholm (G,a,b,y0)),((k + 1) + 1))) . v1 = ((Fredholm (G,a,b,y0)) * (iter ((Fredholm (G,a,b,y0)),(k + 1)))) . v1 by FUNCT_7:71

.= (Fredholm (G,a,b,y0)) . v by A11, FUNCT_1:13 ;

consider f1, g1, Gf1 being continuous PartFunc of REAL, the carrier of X such that

A14: ( 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

A15: ( 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 A18: ( dom Gf1 = ['a,b'] & dom Gf2 = ['a,b'] ) by A14, A15, RELAT_1:27;

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

A20: ['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)) |^ ((k + 1) + 1)) / (((k + 1) + 1) !)) * ||.(u1 - v1).|| )

assume A21: t in ['a,b'] ; :: thesis: ||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ ((k + 1) + 1)) / (((k + 1) + 1) !)) * ||.(u1 - v1).||

then A22: ex g being Real st

( t = g & a <= g & g <= b ) by A20;

a22: ex g being Element of REAL st

( t = g & a <= g & g <= b )

proof

A23: dom Gf12 =
(dom Gf1) /\ (dom Gf2)
by VFUNCT_1:def 2
consider g being Real such that

H1: ( t = g & a <= g & g <= b ) by A21, A20;

reconsider g = g as Element of REAL by XREAL_0:def 1;

take g ; :: thesis: ( t = g & a <= g & g <= b )

thus ( t = g & a <= g & g <= b ) by H1; :: thesis: verum

end;H1: ( t = g & a <= g & g <= b ) by A21, A20;

reconsider g = g as Element of REAL by XREAL_0:def 1;

take g ; :: thesis: ( t = g & a <= g & g <= b )

thus ( t = g & a <= g & g <= b ) by H1; :: thesis: verum

.= ['a,b'] by A18 ;

then A24: dom ||.Gf12.|| = ['a,b'] by NORMSP_0:def 2;

A27: a in ['a,b'] by A20, A1;

( min (a,t) = a & max (a,t) = t ) by A22, XXREAL_0:def 9, XXREAL_0:def 10;

then A30: ( ||.Gf12.|| is_integrable_on ['a,t'] & ||.Gf12.|| | ['a,t'] is bounded & ||.(integral (Gf12,a,t)).|| <= integral (||.Gf12.||,a,t) ) by A1, A23, A27, A21, INTEGR21:22;

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

then consider rg being PartFunc of REAL,REAL such that

A31: ( dom rg = ['a,t'] & ( for x being Real st x in ['a,t'] holds

rg . x = r * ((((r * (x - a)) |^ (k + 1)) / ((k + 1) !)) * ||.(u1 - v1).||) ) & rg is continuous & rg is_integrable_on ['a,t'] & rg | ['a,t'] is bounded & integral (rg,a,t) = (((r * (t - a)) |^ ((k + 1) + 1)) / (((k + 1) + 1) !)) * ||.(u1 - v1).|| ) by Lm7, a22;

A32: ['a,t'] c= ['a,b'] by A22, INTEGR19:1;

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

||.Gf12.|| . x <= rg . x

proof

then A38:
integral (||.Gf12.||,a,t) <= integral (rg,a,t)
by A30, A22, A24, A32, A31, ORDEQ_01:48;
let x be Real; :: thesis: ( x in ['a,t'] implies ||.Gf12.|| . x <= rg . x )

assume A33: x in ['a,t'] ; :: thesis: ||.Gf12.|| . x <= rg . x

then A34: Gf12 /. x = (Gf1 /. x) - (Gf2 /. x) by A23, A32, VFUNCT_1:def 2;

A35: Gf1 /. x = Gf1 . x by A18, A32, A33, PARTFUN1:def 6

.= G . (f1 . x) by A32, A33, A18, A14, FUNCT_1:12

.= G /. (f1 /. x) by A32, A33, A14, PARTFUN1:def 6 ;

Gf2 /. x = Gf2 . x by A18, A32, A33, PARTFUN1:def 6

.= G . (f2 . x) by A32, A33, A18, A15, FUNCT_1:12

.= G /. (f2 /. x) by A32, A33, A15, PARTFUN1:def 6 ;

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

r * ||.((f1 /. x) - (f2 /. x)).|| <= r * ((((r * (x - a)) |^ (k + 1)) / ((k + 1) !)) * ||.(u1 - v1).||) by A1, XREAL_1:64, A9, A14, A15, A32, A33;

then r * ||.((f1 /. x) - (f2 /. x)).|| <= rg . x by A33, A31;

then ||.((Gf1 /. x) - (Gf2 /. x)).|| <= rg . x by A37, XXREAL_0:2;

hence ||.Gf12.|| . x <= rg . x by A24, A32, A33, NORMSP_0:def 2, A34; :: thesis: verum

end;assume A33: x in ['a,t'] ; :: thesis: ||.Gf12.|| . x <= rg . x

then A34: Gf12 /. x = (Gf1 /. x) - (Gf2 /. x) by A23, A32, VFUNCT_1:def 2;

A35: Gf1 /. x = Gf1 . x by A18, A32, A33, PARTFUN1:def 6

.= G . (f1 . x) by A32, A33, A18, A14, FUNCT_1:12

.= G /. (f1 /. x) by A32, A33, A14, PARTFUN1:def 6 ;

Gf2 /. x = Gf2 . x by A18, A32, A33, PARTFUN1:def 6

.= G . (f2 . x) by A32, A33, A18, A15, FUNCT_1:12

.= G /. (f2 /. x) by A32, A33, A15, PARTFUN1:def 6 ;

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

r * ||.((f1 /. x) - (f2 /. x)).|| <= r * ((((r * (x - a)) |^ (k + 1)) / ((k + 1) !)) * ||.(u1 - v1).||) by A1, XREAL_1:64, A9, A14, A15, A32, A33;

then r * ||.((f1 /. x) - (f2 /. x)).|| <= rg . x by A33, A31;

then ||.((Gf1 /. x) - (Gf2 /. x)).|| <= rg . x by A37, XXREAL_0:2;

hence ||.Gf12.|| . x <= rg . x by A24, A32, A33, NORMSP_0:def 2, A34; :: thesis: verum

( g /. t = y0 + (integral (Gf1,a,t)) & h /. t = y0 + (integral (Gf2,a,t)) ) by A14, A15, A21, A12, A10, A13;

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 A18, A27, A21, A1, INTEGR21:30 ;

hence ||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ ((k + 1) + 1)) / (((k + 1) + 1) !)) * ||.(u1 - v1).|| by A38, A30, XXREAL_0:2, A31; :: thesis: verum

hence for m being Element of NAT

for g, h being continuous PartFunc of REAL, the carrier of X st g = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . u1 & h = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . v1 holds

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

||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u1 - v1).|| ; :: thesis: verum