let I, J, K be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for Fz being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & Fz = (Integral2 (L-Meas,(R_EAL g))) | [:I,J:] holds
Fz is_uniformly_continuous_on [:I,J:]
let f be PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for Fz being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & Fz = (Integral2 (L-Meas,(R_EAL g))) | [:I,J:] holds
Fz is_uniformly_continuous_on [:I,J:]
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis: for Fz being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & Fz = (Integral2 (L-Meas,(R_EAL g))) | [:I,J:] holds
Fz is_uniformly_continuous_on [:I,J:]
let Fz be PartFunc of [:RNS_Real,RNS_Real:],RNS_Real; :: thesis: ( [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & Fz = (Integral2 (L-Meas,(R_EAL g))) | [:I,J:] implies Fz is_uniformly_continuous_on [:I,J:] )
assume that
A1: [:[:I,J:],K:] = dom f and
A2: f is_continuous_on [:[:I,J:],K:] and
A3: f = g and
A4: Fz = (Integral2 (L-Meas,(R_EAL g))) | [:I,J:] ; :: thesis: Fz is_uniformly_continuous_on [:I,J:]
dom (Integral2 (L-Meas,(R_EAL g))) = [:REAL,REAL:] by FUNCT_2:def 1;
then A5: dom Fz = [:I,J:] by A4;
reconsider RG = Fz as PartFunc of [:REAL,REAL:],REAL ;
consider s, t being Real such that
A6: K = [.s,t.] by MEASURE5:def 3;
A7: s <= t by A6, XXREAL_1:29;
A8: K = ['s,t'] by A6, INTEGRA5:def 3, XXREAL_1:29;

now :: thesis: for e being Real st 0 < e holds
ex r being Real st
( 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
|.((RG . [x2,y2]) - (RG . [x1,y1])).| < e ) )

let e be Real; :: thesis: ( 0 < e implies ex r being Real st
( 0 < b₂ & ( for x1, x2, y1, y2 being Real st [x2,y2] in [:I,J:] & [y1,b₆] in [:I,J:] & |.(y1 - x2).| < x1 & |.(b₆ - y2).| < x1 holds
|.((RG . [y1,b₆]) - (RG . [x2,y2])).| < r ) ) )
assume A9: 0 < e ; :: thesis: ex r being Real st
( 0 < b₂ & ( for x1, x2, y1, y2 being Real st [x2,y2] in [:I,J:] & [y1,b₆] in [:I,J:] & |.(y1 - x2).| < x1 & |.(b₆ - y2).| < x1 holds
|.((RG . [y1,b₆]) - (RG . [x2,y2])).| < r ) )

per cases ( s = t or s <> t ) ;

suppose A10: s = t ; :: thesis: ex r being Real st
( 0 < b₂ & ( for x1, x2, y1, y2 being Real st [x2,y2] in [:I,J:] & [y1,b₆] in [:I,J:] & |.(y1 - x2).| < x1 & |.(b₆ - y2).| < x1 holds
|.((RG . [y1,b₆]) - (RG . [x2,y2])).| < r ) )

consider r being Real such that
A11: ( 0 < r & ( for u1, u2 being Element of [:REAL,REAL:]
for x1, y1, x2, y2 being Real st u1 = [x1,y1] & u2 = [x2,y2] & |.(x2 - x1).| < r & |.(y2 - y1).| < r & u1 in [:I,J:] & u2 in [:I,J:] holds
for z being Element of REAL st z in K holds
|.(((ProjPMap1 ((R_EAL g),u2)) . z) - ((ProjPMap1 ((R_EAL g),u1)) . z)).| < e ) ) by A1, A2, A3, A9, Th31;
take r = r; :: thesis: ( 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
|.((RG . [x2,y2]) - (RG . [x1,y1])).| < e ) )
thus 0 < r by A11; :: thesis: 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
|.((RG . [x2,y2]) - (RG . [x1,y1])).| < e
thus 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
|.((RG . [x2,y2]) - (RG . [x1,y1])).| < e :: thesis: verum

proof

let x1, x2, y1, y2 be Real; :: thesis: ( [x1,y1] in [:I,J:] & [x2,y2] in [:I,J:] & |.(x2 - x1).| < r & |.(y2 - y1).| < r implies |.((RG . [x2,y2]) - (RG . [x1,y1])).| < e )
assume A12: ( [x1,y1] in [:I,J:] & [x2,y2] in [:I,J:] & |.(x2 - x1).| < r & |.(y2 - y1).| < r ) ; :: thesis: |.((RG . [x2,y2]) - (RG . [x1,y1])).| < e
A13: ( x1 in I & x2 in I & y1 in J & y2 in J ) by A12, ZFMISC_1:87;
reconsider xx1 = x1, xx2 = x2, yy1 = y1, yy2 = y2 as Element of REAL by XREAL_0:def 1;
( x1 in REAL & y1 in REAL ) by XREAL_0:def 1;
then reconsider u1 = [x1,y1] as Element of [:REAL,REAL:] by ZFMISC_1:def 2;
reconsider Pg0 = ProjPMap1 ((R_EAL g),u1) as PartFunc of REAL,REAL by MESFUN16:30;
A14: dom Pg0 = K by A1, A3, A12, MESFUN16:27;
A15: Pg0 is continuous by A1, A2, A3, A13, Th17;
A16: ( Pg0 | K is bounded & Pg0 is_integrable_on K ) by A1, A2, A3, A13, Th21;
A17: (Integral2 (L-Meas,(R_EAL g))) . [x1,y1] = integral (Pg0,K) by A1, A2, A3, A13, Th22;
( x2 in REAL & y2 in REAL ) by XREAL_0:def 1;
then reconsider u2 = [x2,y2] as Element of [:REAL,REAL:] by ZFMISC_1:def 2;
reconsider Pg1 = ProjPMap1 ((R_EAL g),u2) as PartFunc of REAL,REAL by MESFUN16:30;
A18: dom Pg1 = K by A1, A3, A12, MESFUN16:27;
A19: Pg1 is continuous by A1, A2, A3, A13, Th17;
A20: ( Pg1 | K is bounded & Pg1 is_integrable_on K ) by A1, A2, A3, A13, Th21;
A21: (Integral2 (L-Meas,(R_EAL g))) . [x2,y2] = integral (Pg1,K) by A1, A2, A3, A13, Th22;
( RG . u1 = integral (Pg0,K) & RG . u2 = integral (Pg1,K) ) by A4, A12, A17, A21, FUNCT_1:49;
then A22: ( RG . u1 = integral (Pg0,s,t) & RG . u2 = integral (Pg1,s,t) ) by A8, A6, XXREAL_1:29, INTEGRA5:def 4;
A23: dom (Pg1 - Pg0) = (dom Pg1) /\ (dom Pg0) by VALUED_1:12;
then A24: ( (Pg1 - Pg0) | ['s,t'] is bounded & Pg1 - Pg0 is_integrable_on ['s,t'] ) by A8, A14, A15, A18, A19, INTEGRA5:10, INTEGRA5:11;
A25: ( s in ['s,t'] & t in ['s,t'] ) by A6, A7, A8;
for y being Real st y in ['s,t'] holds
|.((Pg1 - Pg0) . y).| <= e

proof

let y be Real; :: thesis: ( y in ['s,t'] implies |.((Pg1 - Pg0) . y).| <= e )
assume A26: y in ['s,t'] ; :: thesis: |.((Pg1 - Pg0) . y).| <= e
then A27: |.(((ProjPMap1 ((R_EAL g),u2)) . y) - ((ProjPMap1 ((R_EAL g),u1)) . y)).| < e by A8, A11, A12;
A28: - ((ProjPMap1 ((R_EAL g),u1)) . y) = - (Pg0 . y) by XXREAL_3:def 3;
((ProjPMap1 ((R_EAL g),u2)) . y) - ((ProjPMap1 ((R_EAL g),u1)) . y) = ((ProjPMap1 ((R_EAL g),u2)) . y) + (- ((ProjPMap1 ((R_EAL g),u1)) . y)) by XXREAL_3:def 4
.= (Pg1 . y) + (- (Pg0 . y)) by A28, XXREAL_3:def 2
.= (Pg1 . y) - (Pg0 . y)
.= (Pg1 - Pg0) . y by A8, A14, A18, A23, A26, VALUED_1:13 ;
hence |.((Pg1 - Pg0) . y).| <= e by A27, EXTREAL1:12; :: thesis: verum

end;

then |.(integral ((Pg1 - Pg0),s,t)).| <= e * (t - s) by A7, A8, A14, A18, A23, A24, A25, INTEGRA6:23;
hence |.((RG . [x2,y2]) - (RG . [x1,y1])).| < e by A10, A9, A22, A8, INTEGRA6:12, A14, A16, A18, A20; :: thesis: verum

end;

end;

suppose s <> t ; :: thesis: ex r being Real st
( 0 < b₂ & ( for x1, x2, y1, y2 being Real st [x2,y2] in [:I,J:] & [y1,b₆] in [:I,J:] & |.(y1 - x2).| < x1 & |.(b₆ - y2).| < x1 holds
|.((RG . [y1,b₆]) - (RG . [x2,y2])).| < r ) )

then A29: s < t by A7, XXREAL_0:1;
set e1 = e / 2;
A30: ( 0 < e / 2 & e / 2 < e ) by A9, XREAL_1:215, XREAL_1:216;
A31: 0 < t - s by A29, XREAL_1:50;
then consider r being Real such that
A32: ( 0 < r & ( for u1, u2 being Element of [:REAL,REAL:]
for x1, y1, x2, y2 being Real st u1 = [x1,y1] & u2 = [x2,y2] & |.(x2 - x1).| < r & |.(y2 - y1).| < r & u1 in [:I,J:] & u2 in [:I,J:] holds
for z being Element of REAL st z in K holds
|.(((ProjPMap1 ((R_EAL g),u2)) . z) - ((ProjPMap1 ((R_EAL g),u1)) . z)).| < (e / 2) / (t - s) ) ) by A1, A2, A3, A30, Th31, XREAL_1:139;
take r = r; :: thesis: ( 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
|.((RG . [x2,y2]) - (RG . [x1,y1])).| < e ) )
thus 0 < r by A32; :: thesis: 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
|.((RG . [x2,y2]) - (RG . [x1,y1])).| < e
let x1, x2, y1, y2 be Real; :: thesis: ( [x1,y1] in [:I,J:] & [x2,y2] in [:I,J:] & |.(x2 - x1).| < r & |.(y2 - y1).| < r implies |.((RG . [x2,y2]) - (RG . [x1,y1])).| < e )
assume A33: ( [x1,y1] in [:I,J:] & [x2,y2] in [:I,J:] & |.(x2 - x1).| < r & |.(y2 - y1).| < r ) ; :: thesis: |.((RG . [x2,y2]) - (RG . [x1,y1])).| < e
then A34: ( x1 in I & x2 in I & y1 in J & y2 in J ) by ZFMISC_1:87;
reconsider xx1 = x1, xx2 = x2, yy1 = y1, yy2 = y2 as Element of REAL by XREAL_0:def 1;
( x1 in REAL & y1 in REAL ) by XREAL_0:def 1;
then reconsider u1 = [x1,y1] as Element of [:REAL,REAL:] by ZFMISC_1:def 2;
reconsider Pg0 = ProjPMap1 ((R_EAL g),u1) as PartFunc of REAL,REAL by MESFUN16:30;
A35: ( dom Pg0 = K & Pg0 is continuous & Pg0 | K is bounded & Pg0 is_integrable_on K & (Integral2 (L-Meas,(R_EAL g))) . [x1,y1] = integral (Pg0,K) ) by A1, A2, A3, A34, A33, Th17, Th21, Th22, MESFUN16:27;
( x2 in REAL & y2 in REAL ) by XREAL_0:def 1;
then reconsider u2 = [x2,y2] as Element of [:REAL,REAL:] by ZFMISC_1:def 2;
reconsider Pg1 = ProjPMap1 ((R_EAL g),u2) as PartFunc of REAL,REAL by MESFUN16:30;
A36: ( dom Pg1 = K & Pg1 is continuous & Pg1 | K is bounded & Pg1 is_integrable_on K & (Integral2 (L-Meas,(R_EAL g))) . [x2,y2] = integral (Pg1,K) ) by A1, A2, A3, A34, A33, Th17, Th21, Th22, MESFUN16:27;
then ( RG . u1 = integral (Pg0,K) & RG . u2 = integral (Pg1,K) ) by A4, A33, A35, FUNCT_1:49;
then ( RG . u1 = integral (Pg0,s,t) & RG . u2 = integral (Pg1,s,t) ) by A8, A6, XXREAL_1:29, INTEGRA5:def 4;
then A37: |.((RG . u2) - (RG . u1)).| = |.(integral ((Pg1 - Pg0),s,t)).| by A8, A7, INTEGRA6:12, A36, A35;
A38: dom (Pg1 - Pg0) = (dom Pg1) /\ (dom Pg0) by VALUED_1:12;
then A39: ( (Pg1 - Pg0) | ['s,t'] is bounded & Pg1 - Pg0 is_integrable_on ['s,t'] ) by A8, A35, A36, INTEGRA5:10, INTEGRA5:11;
A40: ( s in ['s,t'] & t in ['s,t'] ) by A6, A8, A7;
for y being Real st y in ['s,t'] holds
|.((Pg1 - Pg0) . y).| <= (e / 2) / (t - s)

proof

let y be Real; :: thesis: ( y in ['s,t'] implies |.((Pg1 - Pg0) . y).| <= (e / 2) / (t - s) )
assume A41: y in ['s,t'] ; :: thesis: |.((Pg1 - Pg0) . y).| <= (e / 2) / (t - s)
then A42: |.(((ProjPMap1 ((R_EAL g),u2)) . y) - ((ProjPMap1 ((R_EAL g),u1)) . y)).| < (e / 2) / (t - s) by A8, A32, A33;
A43: - ((ProjPMap1 ((R_EAL g),u1)) . y) = - (Pg0 . y) by XXREAL_3:def 3;
((ProjPMap1 ((R_EAL g),u2)) . y) - ((ProjPMap1 ((R_EAL g),u1)) . y) = ((ProjPMap1 ((R_EAL g),u2)) . y) + (- ((ProjPMap1 ((R_EAL g),u1)) . y)) by XXREAL_3:def 4
.= (Pg1 . y) + (- (Pg0 . y)) by A43, XXREAL_3:def 2
.= (Pg1 . y) - (Pg0 . y)
.= (Pg1 - Pg0) . y by A8, A35, A36, A38, A41, VALUED_1:13 ;
hence |.((Pg1 - Pg0) . y).| <= (e / 2) / (t - s) by A42, EXTREAL1:12; :: thesis: verum

end;

then |.(integral ((Pg1 - Pg0),s,t)).| <= ((e / 2) / (t - s)) * (t - s) by A7, A8, A35, A36, A38, A39, A40, INTEGRA6:23;
then |.(integral ((Pg1 - Pg0),s,t)).| <= e / 2 by A31, XCMPLX_1:87;
hence |.((RG . [x2,y2]) - (RG . [x1,y1])).| < e by A30, A37, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence Fz is_uniformly_continuous_on [:I,J:] by A5, MESFUN16:10; :: thesis: verum