let I, J be non empty closed_interval Subset of REAL; :: thesis:
let f be PartFunc of [:RNS_Real,RNS_Real:],RNS_Real; :: thesis:
let g be PartFunc of [:REAL,REAL:],REAL; :: thesis:
let G2 be PartFunc of REAL,REAL; :: thesis:
assume that
A1: [:I,J:] = dom f and
A2: f is_continuous_on [:I,J:] and
A3: f = g and
A4: G2 = (Integral2 (L-Meas,(R_EAL g))) | I ; :: thesis:
consider c, d being Real such that
A5: J = [.c,d.] by MEASURE5:def 3;
A6: c <= d by A5, XXREAL_1:29;
then A7: ( c in J & d in J ) by A5;
A8: [.c,d.] = ['c,d'] by A5, XXREAL_1:29, INTEGRA5:def 3;
A9: for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2 being Real st |.(x2 - x1).| < r & x1 in I & x2 in I holds
for y being Real st y in J holds
|.((g . [x2,y]) - (g . [x1,y])).| < e ) )

let e be Real; :: thesis:
assume 0 < e ; :: thesis:
then consider r being Real such that
A10: ( 0 < r & ( for x1, x2, y1, y2 being Real st [x1,y1] in [:I,J:] & [x2,y2] in [:I,J:] & |.(x2 - x1).| < r & |.(y2 - y1).| < r holds
|.((g . [x2,y2]) - (g . [x1,y1])).| < e ) ) by A2, A3, Th18;
take r ; :: thesis:
thus 0 < r by A10; :: thesis:
let x1, x2 be Real; :: thesis:
assume A11: ( |.(x2 - x1).| < r & x1 in I & x2 in I ) ; :: thesis:
let y be Real; :: thesis:
assume y in J ; :: thesis:
then A12: ( [x1,y] in [:I,J:] & [x2,y] in [:I,J:] ) by A11, ZFMISC_1:87;
|.(y - y).| < r by A10;
hence |.((g . [x2,y]) - (g . [x1,y])).| < e by A10, A11, A12; :: thesis:

end;

set Rg = R_EAL g;
A13: dom (R_EAL g) = [:I,J:] by A1, A3, MESFUNC5:def 7;
A14: for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2 being Element of REAL st |.(x2 - x1).| < r & x1 in I & x2 in I holds
for y being Element of REAL st y in J holds
|.(((ProjPMap1 ((R_EAL g),x2)) . y) - ((ProjPMap1 ((R_EAL g),x1)) . y)).| < e ) )

proof

let e be Real; :: thesis:
assume 0 < e ; :: thesis:
then consider r being Real such that
A15: ( 0 < r & ( for x1, x2 being Real st |.(x2 - x1).| < r & x1 in I & x2 in I holds
for y being Real st y in J holds
|.((g . [x2,y]) - (g . [x1,y])).| < e ) ) by A9;
take r ; :: thesis:
thus 0 < r by A15; :: thesis:
let x1, x2 be Element of REAL ; :: thesis:
assume A16: ( |.(x2 - x1).| < r & x1 in I & x2 in I ) ; :: thesis:
let y be Element of REAL ; :: thesis:
assume A17: y in J ; :: thesis:
then A18: |.((g . [x2,y]) - (g . [x1,y])).| < e by A15, A16;
a18: (g . [x2,y]) - (g . [x1,y]) = (g . [x2,y]) - (g . [x1,y]) ;
( (ProjPMap1 ((R_EAL g),x1)) . y = (R_EAL g) . (x1,y) & (R_EAL g) . (x1,y) = g . [x1,y] & (ProjPMap1 ((R_EAL g),x2)) . y = (R_EAL g) . (x2,y) & (R_EAL g) . (x2,y) = g . [x2,y] ) by A13, A16, A17, ZFMISC_1:87, MESFUN12:def 3, MESFUNC5:def 7;
hence |.(((ProjPMap1 ((R_EAL g),x2)) . y) - ((ProjPMap1 ((R_EAL g),x1)) . y)).| < e by A18, a18, EXTREAL1:12; :: thesis:

end;

set F = Integral2 (L-Meas,(R_EAL g));
A19: dom (Integral2 (L-Meas,(R_EAL g))) = REAL by FUNCT_2:def 1;
for x0, r being Real st x0 in I & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in I & |.(x1 - x0).| < s holds
|.((G2 . x1) - (G2 . x0)).| < r ) )

proof

let xx0, r be Real; :: thesis:
assume A20: ( xx0 in I & 0 < r ) ; :: thesis:
reconsider x0 = xx0 as Element of REAL by XREAL_0:def 1;
reconsider Pg0 = ProjPMap1 ((R_EAL g),x0) as PartFunc of REAL,REAL by Th30;
A21: dom Pg0 = J by A20, A1, A3, Th27;
A22: Pg0 is continuous by A1, A2, A3, Th36;
A23: ( Pg0 | J is bounded & Pg0 is_integrable_on J ) by A20, A1, A2, A3, Th40;
A24: (Integral2 (L-Meas,(R_EAL g))) . x0 = integral (Pg0,J) by A20, A1, A2, A3, Th41;

per cases ;

suppose A25: c = d ; :: thesis:

proof

let xx1 be Real; :: thesis:
assume A27: ( xx1 in I & |.(xx1 - x0).| < s ) ; :: thesis:
reconsider x1 = xx1 as Element of REAL by XREAL_0:def 1;
reconsider Pg1 = ProjPMap1 ((R_EAL g),x1) as PartFunc of REAL,REAL by Th30;
A28: dom Pg1 = J by A27, A1, A3, Th27;
A29: Pg1 is continuous by A1, A2, A3, Th36;
A30: ( Pg1 | J is bounded & Pg1 is_integrable_on J ) by A27, A1, A2, A3, Th40;
(Integral2 (L-Meas,(R_EAL g))) . x1 = integral (Pg1,J) by A27, A1, A2, A3, Th41;
then ( G2 . xx0 = integral (Pg0,J) & G2 . xx1 = integral (Pg1,J) ) by A4, A20, A24, A27, FUNCT_1:49;
then A31: ( G2 . xx0 = integral (Pg0,c,d) & G2 . xx1 = integral (Pg1,c,d) ) by A5, A8, XXREAL_1:29, INTEGRA5:def 4;
A32: dom (Pg1 - Pg0) = J /\ J by A21, A28, VALUED_1:12;
then A33: ( (Pg1 - Pg0) | J is bounded & Pg1 - Pg0 is_integrable_on J ) by A22, A29, INTEGRA5:10, INTEGRA5:11;
for y being Real st y in J holds
|.((Pg1 - Pg0) . y).| <= r

proof

let y be Real; :: thesis:
assume A34: y in J ; :: thesis:
then A35: |.(((ProjPMap1 ((R_EAL g),x1)) . y) - ((ProjPMap1 ((R_EAL g),x0)) . y)).| < r by A26, A27, A20;
A36: - ((ProjPMap1 ((R_EAL g),x0)) . y) = - (Pg0 . y) by XXREAL_3:def 3;
((ProjPMap1 ((R_EAL g),x1)) . y) - ((ProjPMap1 ((R_EAL g),x0)) . y) = ((ProjPMap1 ((R_EAL g),x1)) . y) + (- ((ProjPMap1 ((R_EAL g),x0)) . y)) by XXREAL_3:def 4;
then ((ProjPMap1 ((R_EAL g),x1)) . y) - ((ProjPMap1 ((R_EAL g),x0)) . y) = (Pg1 . y) + (- (Pg0 . y)) by A36, XXREAL_3:def 2;
then ((ProjPMap1 ((R_EAL g),x1)) . y) - ((ProjPMap1 ((R_EAL g),x0)) . y) = (Pg1 . y) - (Pg0 . y) ;
then ((ProjPMap1 ((R_EAL g),x1)) . y) - ((ProjPMap1 ((R_EAL g),x0)) . y) = (Pg1 - Pg0) . y by A32, A34, VALUED_1:13;
hence |.((Pg1 - Pg0) . y).| <= r by A35, EXTREAL1:12; :: thesis:

end;

then |.(integral ((Pg1 - Pg0),c,d)).| <= r * (d - c) by A6, A5, A8, A32, A33, A7, INTEGRA6:23;
hence |.((G2 . xx1) - (G2 . xx0)).| < r by A25, A20, A31, A5, A8, A28, A30, A21, A23, INTEGRA6:12; :: thesis:

end;

hence ex s being Real st
( 0 < s & ( for x1 being Real st x1 in I & |.(x1 - xx0).| < s holds
|.((G2 . x1) - (G2 . xx0)).| < r ) ) by A26; :: thesis:

end;

suppose c <> d ; :: thesis:

then c < d by A6, XXREAL_0:1;
then A37: 0 < d - c by XREAL_1:50;
set r1 = r / 2;
A38: ( 0 < r / 2 & r / 2 < r ) by A20, XREAL_1:215, XREAL_1:216;
consider s being Real such that
A39: ( 0 < s & ( for x1, x2 being Element of REAL st |.(x2 - x1).| < s & x1 in I & x2 in I holds
for y being Element of REAL st y in J holds
|.(((ProjPMap1 ((R_EAL g),x2)) . y) - ((ProjPMap1 ((R_EAL g),x1)) . y)).| < (r / 2) / (d - c) ) ) by A14, XREAL_1:139, A38, A37;
take s ; :: thesis:
thus 0 < s by A39; :: thesis:
let xx1 be Real; :: thesis:
assume A40: ( xx1 in I & |.(xx1 - xx0).| < s ) ; :: thesis:
reconsider x1 = xx1 as Element of REAL by XREAL_0:def 1;
reconsider Pg1 = ProjPMap1 ((R_EAL g),x1) as PartFunc of REAL,REAL by Th30;
A41: dom Pg1 = J by A40, A1, A3, Th27;
A42: Pg1 is continuous by A1, A2, A3, Th36;
A43: ( Pg1 | J is bounded & Pg1 is_integrable_on J ) by A40, A1, A2, A3, Th40;
(Integral2 (L-Meas,(R_EAL g))) . x1 = integral (Pg1,J) by A40, A1, A2, A3, Th41;
then ( G2 . xx0 = integral (Pg0,J) & G2 . xx1 = integral (Pg1,J) ) by A4, A20, A24, A40, FUNCT_1:49;
then ( G2 . xx0 = integral (Pg0,c,d) & G2 . xx1 = integral (Pg1,c,d) ) by A5, A8, XXREAL_1:29, INTEGRA5:def 4;
then A44: |.((G2 . xx1) - (G2 . xx0)).| = |.(integral ((Pg1 - Pg0),c,d)).| by A6, A5, A8, A41, A43, A21, A23, INTEGRA6:12;
A45: dom (Pg1 - Pg0) = J /\ J by A21, A41, VALUED_1:12;
then A46: ( (Pg1 - Pg0) | J is bounded & Pg1 - Pg0 is_integrable_on J ) by A22, A42, INTEGRA5:10, INTEGRA5:11;
for y being Real st y in J holds
|.((Pg1 - Pg0) . y).| <= (r / 2) / (d - c)

proof

let y be Real; :: thesis:
assume A47: y in J ; :: thesis:
then A48: |.(((ProjPMap1 ((R_EAL g),x1)) . y) - ((ProjPMap1 ((R_EAL g),x0)) . y)).| < (r / 2) / (d - c) by A39, A40, A20;
A49: - ((ProjPMap1 ((R_EAL g),x0)) . y) = - (Pg0 . y) by XXREAL_3:def 3;
((ProjPMap1 ((R_EAL g),x1)) . y) - ((ProjPMap1 ((R_EAL g),x0)) . y) = ((ProjPMap1 ((R_EAL g),x1)) . y) + (- ((ProjPMap1 ((R_EAL g),x0)) . y)) by XXREAL_3:def 4;
then ((ProjPMap1 ((R_EAL g),x1)) . y) - ((ProjPMap1 ((R_EAL g),x0)) . y) = (Pg1 . y) + (- (Pg0 . y)) by A49, XXREAL_3:def 2;
then ((ProjPMap1 ((R_EAL g),x1)) . y) - ((ProjPMap1 ((R_EAL g),x0)) . y) = (Pg1 . y) - (Pg0 . y) ;
then ((ProjPMap1 ((R_EAL g),x1)) . y) - ((ProjPMap1 ((R_EAL g),x0)) . y) = (Pg1 - Pg0) . y by A45, A47, VALUED_1:13;
hence |.((Pg1 - Pg0) . y).| <= (r / 2) / (d - c) by A48, EXTREAL1:12; :: thesis:

end;

end;

then G2 | I is continuous by A4, A19, FCONT_1:14;
hence G2 is continuous by A4; :: thesis: