let I, J be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL
for G2 being PartFunc of REAL,REAL st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G2 = (Integral2 (L-Meas,|.(R_EAL g).|)) | I holds
G2 is continuous
let f be PartFunc of [:RNS_Real,RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:REAL,REAL:],REAL
for G2 being PartFunc of REAL,REAL st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G2 = (Integral2 (L-Meas,|.(R_EAL g).|)) | I holds
G2 is continuous
let g be PartFunc of [:REAL,REAL:],REAL; :: thesis: for G2 being PartFunc of REAL,REAL st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G2 = (Integral2 (L-Meas,|.(R_EAL g).|)) | I holds
G2 is continuous
let G2 be PartFunc of REAL,REAL; :: thesis: ( [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G2 = (Integral2 (L-Meas,|.(R_EAL g).|)) | I implies G2 is continuous )
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: G2 is continuous
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 ) )

proof

let e be Real; :: thesis: ( 0 < e implies 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 ) ) )
assume 0 < e ; :: thesis: 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 ) )
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, Th23;
take r ; :: thesis: ( 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 ) )
thus 0 < r by A10; :: thesis: 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 x1, x2 be Real; :: thesis: ( |.(x2 - x1).| < r & x1 in I & x2 in I implies for y being Real st y in J holds
|.((|.g.| . [x2,y]) - (|.g.| . [x1,y])).| < e )
assume A11: ( |.(x2 - x1).| < r & x1 in I & x2 in I ) ; :: thesis: for y being Real st y in J holds
|.((|.g.| . [x2,y]) - (|.g.| . [x1,y])).| < e
let y be Real; :: thesis: ( y in J implies |.((|.g.| . [x2,y]) - (|.g.| . [x1,y])).| < e )
assume y in J ; :: thesis: |.((|.g.| . [x2,y]) - (|.g.| . [x1,y])).| < e
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: verum

end;

set Rg = R_EAL g;
dom |.(R_EAL g).| = dom (R_EAL g) by MESFUNC1:def 10;
then A13: dom |.(R_EAL g).| = [:I,J:] by A1, A3, MESFUNC5:def 7;
A14: for x, y being Element of REAL st x in I & y in J holds
( (ProjPMap1 (|.(R_EAL g).|,x)) . y = |.(R_EAL g).| . (x,y) & |.(R_EAL g).| . (x,y) = |.(g . [x,y]).| & |.(R_EAL g).| . (x,y) = |.g.| . [x,y] )

proof

let x, y be Element of REAL ; :: thesis: ( x in I & y in J implies ( (ProjPMap1 (|.(R_EAL g).|,x)) . y = |.(R_EAL g).| . (x,y) & |.(R_EAL g).| . (x,y) = |.(g . [x,y]).| & |.(R_EAL g).| . (x,y) = |.g.| . [x,y] ) )
assume A15: ( x in I & y in J ) ; :: thesis: ( (ProjPMap1 (|.(R_EAL g).|,x)) . y = |.(R_EAL g).| . (x,y) & |.(R_EAL g).| . (x,y) = |.(g . [x,y]).| & |.(R_EAL g).| . (x,y) = |.g.| . [x,y] )
hence (ProjPMap1 (|.(R_EAL g).|,x)) . y = |.(R_EAL g).| . (x,y) by A13, ZFMISC_1:87, MESFUN12:def 3; :: thesis: ( |.(R_EAL g).| . (x,y) = |.(g . [x,y]).| & |.(R_EAL g).| . (x,y) = |.g.| . [x,y] )
[x,y] in dom g by A15, A1, A3, ZFMISC_1:87;
then A16: [x,y] in dom |.g.| by VALUED_1:def 11;
A17: (R_EAL g) . [x,y] = g . [x,y] by MESFUNC5:def 7;
|.(R_EAL g).| . (x,y) = |.((R_EAL g) . [x,y]).| by A15, A13, ZFMISC_1:87, MESFUNC1:def 10;
hence |.(R_EAL g).| . (x,y) = |.(g . [x,y]).| by A17, EXTREAL1:12; :: thesis: |.(R_EAL g).| . (x,y) = |.g.| . [x,y]
hence |.(R_EAL g).| . (x,y) = |.g.| . [x,y] by VALUED_1:def 11, A16; :: thesis: verum

end;

A18: 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: ( 0 < e implies 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 ) ) )
assume 0 < e ; :: thesis: 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 ) )
then consider r being Real such that
A19: ( 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: ( 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 ) )
thus 0 < r by A19; :: thesis: 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
let x1, x2 be Element of REAL ; :: thesis: ( |.(x2 - x1).| < r & x1 in I & x2 in I implies for y being Element of REAL st y in J holds
|.(((ProjPMap1 (|.(R_EAL g).|,x2)) . y) - ((ProjPMap1 (|.(R_EAL g).|,x1)) . y)).| < e )
assume A20: ( |.(x2 - x1).| < r & x1 in I & x2 in I ) ; :: thesis: for y being Element of REAL st y in J holds
|.(((ProjPMap1 (|.(R_EAL g).|,x2)) . y) - ((ProjPMap1 (|.(R_EAL g).|,x1)) . y)).| < e
let y be Element of REAL ; :: thesis: ( y in J implies |.(((ProjPMap1 (|.(R_EAL g).|,x2)) . y) - ((ProjPMap1 (|.(R_EAL g).|,x1)) . y)).| < e )
assume A21: y in J ; :: thesis: |.(((ProjPMap1 (|.(R_EAL g).|,x2)) . y) - ((ProjPMap1 (|.(R_EAL g).|,x1)) . y)).| < e
then A22: |.((|.g.| . [x2,y]) - (|.g.| . [x1,y])).| < e by A19, A20;
a22: (|.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 A14, A20, A21;
hence |.(((ProjPMap1 (|.(R_EAL g).|,x2)) . y) - ((ProjPMap1 (|.(R_EAL g).|,x1)) . y)).| < e by A22, a22, EXTREAL1:12; :: thesis: verum

end;

set F = Integral2 (L-Meas,|.(R_EAL g).|);
A23: 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: ( xx0 in I & 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Real st x1 in I & |.(x1 - xx0).| < s holds
|.((G2 . x1) - (G2 . xx0)).| < r ) ) )
assume A24: ( xx0 in I & 0 < r ) ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Real st x1 in I & |.(x1 - xx0).| < s holds
|.((G2 . x1) - (G2 . xx0)).| < r ) )
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;
A25: dom Pg0 = J by A24, A1, A3, Th27;
A26: Pg0 | (dom Pg0) is continuous by A1, A2, A3, Th38;
A27: ( Pg0 | J is bounded & Pg0 is_integrable_on J ) by A24, A1, A2, A3, Th44;
A28: (Integral2 (L-Meas,|.(R_EAL g).|)) . x0 = integral (Pg0,J) by A24, A1, A2, A3, Th46;

per cases ( c = d or c <> d ) ;

suppose A29: c = d ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Real st x1 in I & |.(x1 - xx0).| < s holds
|.((G2 . x1) - (G2 . xx0)).| < r ) )

consider s being Real such that
A30: ( 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 ) ) by A18, A24;
for x1 being Real st x1 in I & |.(x1 - x0).| < s holds
|.((G2 . x1) - (G2 . xx0)).| < r

proof

let xx1 be Real; :: thesis: ( xx1 in I & |.(xx1 - x0).| < s implies |.((G2 . xx1) - (G2 . xx0)).| < r )
assume A31: ( xx1 in I & |.(xx1 - x0).| < s ) ; :: thesis: |.((G2 . xx1) - (G2 . xx0)).| < r
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;
A32: dom Pg1 = J by A31, A1, A3, Th27;
A33: Pg1 | (dom Pg1) is continuous by A1, A2, A3, Th38;
A34: ( Pg1 | J is bounded & Pg1 is_integrable_on J ) by A31, A1, A2, A3, Th44;
(Integral2 (L-Meas,|.(R_EAL g).|)) . x1 = integral (Pg1,J) by A31, A1, A2, A3, Th46;
then ( G2 . xx0 = integral (Pg0,J) & G2 . xx1 = integral (Pg1,J) ) by A4, A24, A28, A31, FUNCT_1:49;
then A35: ( G2 . xx0 = integral (Pg0,c,d) & G2 . xx1 = integral (Pg1,c,d) ) by A5, A8, XXREAL_1:29, INTEGRA5:def 4;
A36: dom (Pg1 - Pg0) = J /\ J by A25, A32, VALUED_1:12;
then A37: ( (Pg1 - Pg0) | J is bounded & Pg1 - Pg0 is_integrable_on J ) by A26, A33, INTEGRA5:10, INTEGRA5:11;
for y being Real st y in J holds
|.((Pg1 - Pg0) . y).| <= r

proof

let y be Real; :: thesis: ( y in J implies |.((Pg1 - Pg0) . y).| <= r )
assume A38: y in J ; :: thesis: |.((Pg1 - Pg0) . y).| <= r
then A39: |.(((ProjPMap1 (|.(R_EAL g).|,x1)) . y) - ((ProjPMap1 (|.(R_EAL g).|,x0)) . y)).| < r by A30, A31, A24;
A40: - ((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 A40, 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 A36, A38, VALUED_1:13;
hence |.((Pg1 - Pg0) . y).| <= r by A39, EXTREAL1:12; :: thesis: verum

end;

then |.(integral ((Pg1 - Pg0),c,d)).| <= r * (d - c) by A6, A5, A8, A36, A37, A7, INTEGRA6:23;
hence |.((G2 . xx1) - (G2 . xx0)).| < r by A29, A24, A35, A5, A8, A32, A34, A25, A27, INTEGRA6:12; :: thesis: verum

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 A30; :: thesis: verum

end;

suppose c <> d ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Real st x1 in I & |.(x1 - xx0).| < s holds
|.((G2 . x1) - (G2 . xx0)).| < r ) )

then c < d by A6, XXREAL_0:1;
then A41: 0 < d - c by XREAL_1:50;
set r1 = r / 2;
A42: ( 0 < r / 2 & r / 2 < r ) by A24, XREAL_1:215, XREAL_1:216;
consider s being Real such that
A43: ( 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 A18, XREAL_1:139, A42, A41;
take s ; :: thesis: ( 0 < s & ( for x1 being Real st x1 in I & |.(x1 - xx0).| < s holds
|.((G2 . x1) - (G2 . xx0)).| < r ) )
thus 0 < s by A43; :: thesis: for x1 being Real st x1 in I & |.(x1 - xx0).| < s holds
|.((G2 . x1) - (G2 . xx0)).| < r
let xx1 be Real; :: thesis: ( xx1 in I & |.(xx1 - xx0).| < s implies |.((G2 . xx1) - (G2 . xx0)).| < r )
assume A44: ( xx1 in I & |.(xx1 - xx0).| < s ) ; :: thesis: |.((G2 . xx1) - (G2 . xx0)).| < r
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;
A45: dom Pg1 = J by A44, A1, A3, Th27;
A46: Pg1 | (dom Pg1) is continuous by A1, A2, A3, Th38;
A47: ( Pg1 | J is bounded & Pg1 is_integrable_on J ) by A44, A1, A2, A3, Th44;
(Integral2 (L-Meas,|.(R_EAL g).|)) . x1 = integral (Pg1,J) by A44, A1, A2, A3, Th46;
then ( G2 . xx0 = integral (Pg0,J) & G2 . xx1 = integral (Pg1,J) ) by A4, A24, A28, A44, 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 A48: |.((G2 . xx1) - (G2 . xx0)).| = |.(integral ((Pg1 - Pg0),c,d)).| by A6, A5, A8, A45, A47, A25, A27, INTEGRA6:12;
A49: dom (Pg1 - Pg0) = J /\ J by A25, A45, VALUED_1:12;
then A50: ( (Pg1 - Pg0) | J is bounded & Pg1 - Pg0 is_integrable_on J ) by A26, A46, 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: ( y in J implies |.((Pg1 - Pg0) . y).| <= (r / 2) / (d - c) )
assume A51: y in J ; :: thesis: |.((Pg1 - Pg0) . y).| <= (r / 2) / (d - c)
then A52: |.(((ProjPMap1 (|.(R_EAL g).|,x1)) . y) - ((ProjPMap1 (|.(R_EAL g).|,x0)) . y)).| < (r / 2) / (d - c) by A43, A44, A24;
A53: - ((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 A53, 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 A49, A51, VALUED_1:13;
hence |.((Pg1 - Pg0) . y).| <= (r / 2) / (d - c) by A52, EXTREAL1:12; :: thesis: verum

end;

then |.(integral ((Pg1 - Pg0),c,d)).| <= ((r / 2) / (d - c)) * (d - c) by A6, A5, A8, A49, A50, A7, INTEGRA6:23;
then |.(integral ((Pg1 - Pg0),c,d)).| <= r / 2 by A41, XCMPLX_1:87;
hence |.((G2 . xx1) - (G2 . xx0)).| < r by A48, XXREAL_0:2, A42; :: thesis: verum

end;

end;

end;

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