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 G1 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: G1 = (Integral1 (L-Meas,|.(R_EAL g).|)) | J ; :: thesis:
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 ) )

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, Th23;
take r ; :: thesis:
thus 0 < r by A10; :: thesis:
let y1, y2 be Real; :: thesis:
assume A11: ( |.(y2 - y1).| < r & y1 in J & y2 in J ) ; :: thesis:
let x be Real; :: thesis:
assume x in I ; :: thesis:
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:

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
( (ProjPMap2 (|.(R_EAL g).|,y)) . x = |.(R_EAL g).| . (x,y) & |.(R_EAL g).| . (x,y) = |.(g . [x,y]).| & |.(R_EAL g).| . (x,y) = |.g.| . [x,y] )

proof

end;

proof

let e be Real; :: thesis:
assume 0 < e ; :: thesis:
then consider r being Real such that
A19: ( 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:
thus 0 < r by A19; :: thesis:
let y1, y2 be Element of REAL ; :: thesis:
assume A20: ( |.(y2 - y1).| < r & y1 in J & y2 in J ) ; :: thesis:
let x be Element of REAL ; :: thesis:
assume A21: x in I ; :: thesis:
then A22: |.((|.g.| . [x,y2]) - (|.g.| . [x,y1])).| < e by A19, A20;
a22: (|.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 A14, A20, A21;
hence |.(((ProjPMap2 (|.(R_EAL g).|,y2)) . x) - ((ProjPMap2 (|.(R_EAL g).|,y1)) . x)).| < e by A22, a22, EXTREAL1:12; :: thesis:

end;

proof

let yy0, r be Real; :: thesis:
assume A24: ( yy0 in J & 0 < r ) ; :: thesis:
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;
A25: dom Pg0 = I by A24, A1, A3, Th28;
A26: Pg0 | (dom Pg0) is continuous by A1, A2, A3, Th39;
A27: ( Pg0 | I is bounded & Pg0 is_integrable_on I ) by A24, A1, A2, A3, Th47;
A28: (Integral1 (L-Meas,|.(R_EAL g).|)) . y0 = integral (Pg0,I) by A24, A1, A2, A3, Th49;

per cases ;

suppose A29: a = b ; :: thesis:

proof

let yy1 be Real; :: thesis:
assume A31: ( yy1 in J & |.(yy1 - y0).| < s ) ; :: thesis:
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;
A32: dom Pg1 = I by A31, A1, A3, Th28;
A33: Pg1 | (dom Pg1) is continuous by A1, A2, A3, Th39;
A34: ( Pg1 | I is bounded & Pg1 is_integrable_on I ) by A31, A1, A2, A3, Th47;
(Integral1 (L-Meas,|.(R_EAL g).|)) . y1 = integral (Pg1,I) by A31, A1, A2, A3, Th49;
then ( G1 . yy0 = integral (Pg0,I) & G1 . yy1 = integral (Pg1,I) ) by A4, A24, A28, A31, FUNCT_1:49;
then A35: ( G1 . yy0 = integral (Pg0,a,b) & G1 . yy1 = integral (Pg1,a,b) ) by A5, A8, XXREAL_1:29, INTEGRA5:def 4;
A36: dom (Pg1 - Pg0) = I /\ I by A25, A32, VALUED_1:12;
then A37: ( (Pg1 - Pg0) | I is bounded & Pg1 - Pg0 is_integrable_on I ) by A26, A33, INTEGRA5:10, INTEGRA5:11;
for x being Real st x in I holds
|.((Pg1 - Pg0) . x).| <= r

proof

end;

then |.(integral ((Pg1 - Pg0),a,b)).| <= r * (b - a) by A6, A5, A8, A36, A37, A7, INTEGRA6:23;
hence |.((G1 . yy1) - (G1 . yy0)).| < r by A29, A24, A35, A5, A8, A32, A34, A25, A27, INTEGRA6:12; :: thesis:

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

end;

suppose a <> b ; :: thesis:

then a < b by A6, XXREAL_0:1;
then A41: 0 < b - a 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 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 A18, XREAL_1:139, A42, A41;
take s ; :: thesis:
thus 0 < s by A43; :: thesis:
let yy1 be Real; :: thesis:
assume A44: ( yy1 in J & |.(yy1 - yy0).| < s ) ; :: thesis:
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;
A45: dom Pg1 = I by A44, A1, A3, Th28;
A46: Pg1 | (dom Pg1) is continuous by A1, A2, A3, Th39;
A47: ( Pg1 | I is bounded & Pg1 is_integrable_on I ) by A44, A1, A2, A3, Th47;
(Integral1 (L-Meas,|.(R_EAL g).|)) . y1 = integral (Pg1,I) by A44, A1, A2, A3, Th49;
then ( G1 . yy0 = integral (Pg0,I) & G1 . yy1 = integral (Pg1,I) ) by A4, A24, A28, A44, 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 A48: |.((G1 . yy1) - (G1 . yy0)).| = |.(integral ((Pg1 - Pg0),a,b)).| by A6, A5, A8, A45, A47, A25, A27, INTEGRA6:12;
A49: dom (Pg1 - Pg0) = I /\ I by A25, A45, VALUED_1:12;
then A50: ( (Pg1 - Pg0) | I is bounded & Pg1 - Pg0 is_integrable_on I ) by A26, A46, INTEGRA5:10, INTEGRA5:11;
for x being Real st x in I holds
|.((Pg1 - Pg0) . x).| <= (r / 2) / (b - a)

proof

end;

end;

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