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 G1 being PartFunc of REAL,REAL st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G1 = (Integral1 (L-Meas,(R_EAL g))) | J holds
G1 is continuous
let f be PartFunc of [:RNS_Real,RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:REAL,REAL:],REAL
for G1 being PartFunc of REAL,REAL st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G1 = (Integral1 (L-Meas,(R_EAL g))) | J holds
G1 is continuous
let g be PartFunc of [:REAL,REAL:],REAL; :: thesis: for G1 being PartFunc of REAL,REAL st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G1 = (Integral1 (L-Meas,(R_EAL g))) | J holds
G1 is continuous
let G1 be PartFunc of REAL,REAL; :: thesis: ( [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G1 = (Integral1 (L-Meas,(R_EAL g))) | J implies G1 is continuous )
assume that
A1: [:I,J:] = dom f and
A2: f is_continuous_on [:I,J:] and
A3: f = g and
A4: G1 = (Integral1 (L-Meas,(R_EAL g))) | J ; :: thesis: G1 is continuous
consider a, b being Real such that
A5: I = [.a,b.] by MEASURE5:def 3;
A6: a <= b by A5, XXREAL_1:29;
then A7: ( a in I & b in I ) by A5;
A8: [.a,b.] = ['a,b'] 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 y1, y2 being Real st |.(y2 - y1).| < r & y1 in J & y2 in J holds
for x being Real st x in I holds
|.((g . [x,y2]) - (g . [x,y1])).| < e ) )

proof

let e be Real; :: thesis: ( 0 < e implies ex r being Real st
( 0 < r & ( for y1, y2 being Real st |.(y2 - y1).| < r & y1 in J & y2 in J holds
for x being Real st x in I holds
|.((g . [x,y2]) - (g . [x,y1])).| < e ) ) )
assume 0 < e ; :: thesis: ex r being Real st
( 0 < r & ( for y1, y2 being Real st |.(y2 - y1).| < r & y1 in J & y2 in J holds
for x being Real st x in I holds
|.((g . [x,y2]) - (g . [x,y1])).| < 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, Th18;
take r ; :: thesis: ( 0 < r & ( for y1, y2 being Real st |.(y2 - y1).| < r & y1 in J & y2 in J holds
for x being Real st x in I holds
|.((g . [x,y2]) - (g . [x,y1])).| < e ) )
thus 0 < r by A10; :: thesis: for y1, y2 being Real st |.(y2 - y1).| < r & y1 in J & y2 in J holds
for x being Real st x in I holds
|.((g . [x,y2]) - (g . [x,y1])).| < e
let y1, y2 be Real; :: thesis: ( |.(y2 - y1).| < r & y1 in J & y2 in J implies for x being Real st x in I holds
|.((g . [x,y2]) - (g . [x,y1])).| < e )
assume A11: ( |.(y2 - y1).| < r & y1 in J & y2 in J ) ; :: thesis: for x being Real st x in I holds
|.((g . [x,y2]) - (g . [x,y1])).| < e
let x be Real; :: thesis: ( x in I implies |.((g . [x,y2]) - (g . [x,y1])).| < e )
assume x in I ; :: thesis: |.((g . [x,y2]) - (g . [x,y1])).| < e
then A12: ( [x,y1] in [:I,J:] & [x,y2] in [:I,J:] ) by A11, ZFMISC_1:87;
|.(x - x).| < r by A10;
hence |.((g . [x,y2]) - (g . [x,y1])).| < e by A10, A11, A12; :: thesis: verum

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 y1, y2 being Element of REAL st |.(y2 - y1).| < r & y1 in J & y2 in J holds
for x being Element of REAL st x in I holds
|.(((ProjPMap2 ((R_EAL g),y2)) . x) - ((ProjPMap2 ((R_EAL g),y1)) . x)).| < e ) )

proof

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

end;

set T = Integral1 (L-Meas,(R_EAL g));
A19: dom (Integral1 (L-Meas,(R_EAL g))) = REAL by FUNCT_2:def 1;
for y0, r being Real st y0 in J & 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Real st y1 in J & |.(y1 - y0).| < s holds
|.((G1 . y1) - (G1 . y0)).| < r ) )

proof

let yy0, r be Real; :: thesis: ( yy0 in J & 0 < r implies ex s being Real st
( 0 < s & ( for y1 being Real st y1 in J & |.(y1 - yy0).| < s holds
|.((G1 . y1) - (G1 . yy0)).| < r ) ) )
assume A20: ( yy0 in J & 0 < r ) ; :: thesis: ex s being Real st
( 0 < s & ( for y1 being Real st y1 in J & |.(y1 - yy0).| < s holds
|.((G1 . y1) - (G1 . yy0)).| < r ) )
reconsider y0 = yy0 as Element of REAL by XREAL_0:def 1;
reconsider Pg0 = ProjPMap2 ((R_EAL g),y0) as PartFunc of REAL,REAL by Th30;
A21: dom Pg0 = I by A20, A1, A3, Th28;
A22: Pg0 is continuous by A1, A2, A3, Th37;
A23: ( Pg0 | I is bounded & Pg0 is_integrable_on I ) by A20, A1, A2, A3, Th42;
A24: (Integral1 (L-Meas,(R_EAL g))) . y0 = integral (Pg0,I) by A20, A1, A2, A3, Th43;

per cases ( a = b or a <> b ) ;

suppose A25: a = b ; :: thesis: ex s being Real st
( 0 < s & ( for y1 being Real st y1 in J & |.(y1 - yy0).| < s holds
|.((G1 . y1) - (G1 . yy0)).| < r ) )

consider s being Real such that
A26: ( 0 < s & ( for y1, y2 being Element of REAL st |.(y2 - y1).| < s & y1 in J & y2 in J holds
for x being Element of REAL st x in I holds
|.(((ProjPMap2 ((R_EAL g),y2)) . x) - ((ProjPMap2 ((R_EAL g),y1)) . x)).| < r ) ) by A14, A20;
for y1 being Real st y1 in J & |.(y1 - y0).| < s holds
|.((G1 . y1) - (G1 . yy0)).| < r

proof

let yy1 be Real; :: thesis: ( yy1 in J & |.(yy1 - y0).| < s implies |.((G1 . yy1) - (G1 . yy0)).| < r )
assume A27: ( yy1 in J & |.(yy1 - y0).| < s ) ; :: thesis: |.((G1 . yy1) - (G1 . yy0)).| < r
reconsider y1 = yy1 as Element of REAL by XREAL_0:def 1;
reconsider Pg1 = ProjPMap2 ((R_EAL g),y1) as PartFunc of REAL,REAL by Th30;
A28: dom Pg1 = I by A27, A1, A3, Th28;
A29: Pg1 is continuous by A1, A2, A3, Th37;
A30: ( Pg1 | I is bounded & Pg1 is_integrable_on I ) by A27, A1, A2, A3, Th42;
(Integral1 (L-Meas,(R_EAL g))) . y1 = integral (Pg1,I) by A27, A1, A2, A3, Th43;
then ( G1 . yy0 = integral (Pg0,I) & G1 . yy1 = integral (Pg1,I) ) by A4, A20, A24, A27, FUNCT_1:49;
then A31: ( G1 . yy0 = integral (Pg0,a,b) & G1 . yy1 = integral (Pg1,a,b) ) by A5, A8, XXREAL_1:29, INTEGRA5:def 4;
A32: dom (Pg1 - Pg0) = I /\ I by A21, A28, VALUED_1:12;
then A33: ( (Pg1 - Pg0) | I is bounded & Pg1 - Pg0 is_integrable_on I ) by A22, A29, INTEGRA5:10, INTEGRA5:11;
for x being Real st x in I holds
|.((Pg1 - Pg0) . x).| <= r

proof

let x be Real; :: thesis: ( x in I implies |.((Pg1 - Pg0) . x).| <= r )
assume A34: x in I ; :: thesis: |.((Pg1 - Pg0) . x).| <= r
then A35: |.(((ProjPMap2 ((R_EAL g),y1)) . x) - ((ProjPMap2 ((R_EAL g),y0)) . x)).| < r by A26, A27, A20;
A36: - ((ProjPMap2 ((R_EAL g),y0)) . x) = - (Pg0 . x) by XXREAL_3:def 3;
((ProjPMap2 ((R_EAL g),y1)) . x) - ((ProjPMap2 ((R_EAL g),y0)) . x) = ((ProjPMap2 ((R_EAL g),y1)) . x) + (- ((ProjPMap2 ((R_EAL g),y0)) . x)) by XXREAL_3:def 4;
then ((ProjPMap2 ((R_EAL g),y1)) . x) - ((ProjPMap2 ((R_EAL g),y0)) . x) = (Pg1 . x) + (- (Pg0 . x)) by A36, XXREAL_3:def 2;
then ((ProjPMap2 ((R_EAL g),y1)) . x) - ((ProjPMap2 ((R_EAL g),y0)) . x) = (Pg1 . x) - (Pg0 . x) ;
then ((ProjPMap2 ((R_EAL g),y1)) . x) - ((ProjPMap2 ((R_EAL g),y0)) . x) = (Pg1 - Pg0) . x by A32, A34, VALUED_1:13;
hence |.((Pg1 - Pg0) . x).| <= r by A35, EXTREAL1:12; :: thesis: verum

end;

then |.(integral ((Pg1 - Pg0),a,b)).| <= r * (b - a) by A6, A5, A8, A32, A33, A7, INTEGRA6:23;
hence |.((G1 . yy1) - (G1 . yy0)).| < r by A25, A20, A31, A5, A8, A28, A30, A21, A23, INTEGRA6:12; :: thesis: verum

end;

hence ex s being Real st
( 0 < s & ( for y1 being Real st y1 in J & |.(y1 - yy0).| < s holds
|.((G1 . y1) - (G1 . yy0)).| < r ) ) by A26; :: thesis: verum

end;

suppose a <> b ; :: thesis: ex s being Real st
( 0 < s & ( for y1 being Real st y1 in J & |.(y1 - yy0).| < s holds
|.((G1 . y1) - (G1 . yy0)).| < r ) )

then a < b by A6, XXREAL_0:1;
then A37: 0 < b - a 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 y1, y2 being Element of REAL st |.(y2 - y1).| < s & y1 in J & y2 in J holds
for x being Element of REAL st x in I holds
|.(((ProjPMap2 ((R_EAL g),y2)) . x) - ((ProjPMap2 ((R_EAL g),y1)) . x)).| < (r / 2) / (b - a) ) ) by A14, XREAL_1:139, A38, A37;
take s ; :: thesis: ( 0 < s & ( for y1 being Real st y1 in J & |.(y1 - yy0).| < s holds
|.((G1 . y1) - (G1 . yy0)).| < r ) )
thus 0 < s by A39; :: thesis: for y1 being Real st y1 in J & |.(y1 - yy0).| < s holds
|.((G1 . y1) - (G1 . yy0)).| < r
let yy1 be Real; :: thesis: ( yy1 in J & |.(yy1 - yy0).| < s implies |.((G1 . yy1) - (G1 . yy0)).| < r )
assume A40: ( yy1 in J & |.(yy1 - yy0).| < s ) ; :: thesis: |.((G1 . yy1) - (G1 . yy0)).| < r
reconsider y1 = yy1 as Element of REAL by XREAL_0:def 1;
reconsider Pg1 = ProjPMap2 ((R_EAL g),y1) as PartFunc of REAL,REAL by Th30;
A41: dom Pg1 = I by A40, A1, A3, Th28;
A42: Pg1 is continuous by A1, A2, A3, Th37;
A43: ( Pg1 | I is bounded & Pg1 is_integrable_on I ) by A40, A1, A2, A3, Th42;
(Integral1 (L-Meas,(R_EAL g))) . y1 = integral (Pg1,I) by A40, A1, A2, A3, Th43;
then ( G1 . yy0 = integral (Pg0,I) & G1 . yy1 = integral (Pg1,I) ) by A4, A20, A24, A40, FUNCT_1:49;
then ( G1 . yy0 = integral (Pg0,a,b) & G1 . yy1 = integral (Pg1,a,b) ) by A5, A8, XXREAL_1:29, INTEGRA5:def 4;
then A44: |.((G1 . yy1) - (G1 . yy0)).| = |.(integral ((Pg1 - Pg0),a,b)).| by A6, A5, A8, A41, A43, A21, A23, INTEGRA6:12;
A45: dom (Pg1 - Pg0) = I /\ I by A21, A41, VALUED_1:12;
then A46: ( (Pg1 - Pg0) | I is bounded & Pg1 - Pg0 is_integrable_on I ) by A22, A42, INTEGRA5:10, INTEGRA5:11;
for x being Real st x in I holds
|.((Pg1 - Pg0) . x).| <= (r / 2) / (b - a)

proof

let x be Real; :: thesis: ( x in I implies |.((Pg1 - Pg0) . x).| <= (r / 2) / (b - a) )
assume A47: x in I ; :: thesis: |.((Pg1 - Pg0) . x).| <= (r / 2) / (b - a)
A48: |.(((ProjPMap2 ((R_EAL g),y1)) . x) - ((ProjPMap2 ((R_EAL g),y0)) . x)).| < (r / 2) / (b - a) by A39, A40, A20, A47;
A49: - ((ProjPMap2 ((R_EAL g),y0)) . x) = - (Pg0 . x) by XXREAL_3:def 3;
((ProjPMap2 ((R_EAL g),y1)) . x) - ((ProjPMap2 ((R_EAL g),y0)) . x) = ((ProjPMap2 ((R_EAL g),y1)) . x) + (- ((ProjPMap2 ((R_EAL g),y0)) . x)) by XXREAL_3:def 4;
then ((ProjPMap2 ((R_EAL g),y1)) . x) - ((ProjPMap2 ((R_EAL g),y0)) . x) = (Pg1 . x) + (- (Pg0 . x)) by A49, XXREAL_3:def 2;
then ((ProjPMap2 ((R_EAL g),y1)) . x) - ((ProjPMap2 ((R_EAL g),y0)) . x) = (Pg1 . x) - (Pg0 . x) ;
then ((ProjPMap2 ((R_EAL g),y1)) . x) - ((ProjPMap2 ((R_EAL g),y0)) . x) = (Pg1 - Pg0) . x by A45, A47, VALUED_1:13;
hence |.((Pg1 - Pg0) . x).| <= (r / 2) / (b - a) by A48, EXTREAL1:12; :: thesis: verum

end;

then |.(integral ((Pg1 - Pg0),a,b)).| <= ((r / 2) / (b - a)) * (b - a) by A6, A5, A7, A8, A45, A46, INTEGRA6:23;
then |.(integral ((Pg1 - Pg0),a,b)).| <= r / 2 by A37, XCMPLX_1:87;
hence |.((G1 . yy1) - (G1 . yy0)).| < r by A44, XXREAL_0:2, A38; :: thesis: verum

end;

end;

end;

then G1 | J is continuous by A4, A19, FCONT_1:14;
hence G1 is continuous by A4; :: thesis: verum