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 G = 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;
A9: ( s in K & t in K ) by A6, A7;
A10: K is Element of L-Field by MEASUR10:5, MEASUR12:75;

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
|.((G . [x2,y2]) - (G . [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
|.((G . [y1,b₆]) - (G . [x2,y2])).| < r ) ) )
assume A11: 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
|.((G . [y1,b₆]) - (G . [x2,y2])).| < r ) )

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

suppose A12: 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
|.((G . [y1,b₆]) - (G . [x2,y2])).| < r ) )

consider r being Real such that
A13: ( 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, A11, Th30;
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
|.((G . [x2,y2]) - (G . [x1,y1])).| < e ) )
thus 0 < r by A13; :: 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
|.((G . [x2,y2]) - (G . [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
|.((G . [x2,y2]) - (G . [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 |.((G . [x2,y2]) - (G . [x1,y1])).| < e )
assume A14: ( [x1,y1] in [:I,J:] & [x2,y2] in [:I,J:] & |.(x2 - x1).| < r & |.(y2 - y1).| < r ) ; :: thesis: |.((G . [x2,y2]) - (G . [x1,y1])).| < e
A15: ( x1 in I & x2 in I & y1 in J & y2 in J ) by A14, ZFMISC_1:87;
reconsider xx1 = x1, xx2 = x2, yy1 = y1, yy2 = y2 as Element of REAL by XREAL_0:def 1;
reconsider u1 = [xx1,yy1] as Element of [:REAL,REAL:] ;
reconsider Pg0 = ProjPMap1 (|.(R_EAL g).|,u1) as PartFunc of REAL,REAL by MESFUN16:30;
A16: dom Pg0 = K by A1, A3, A14, MESFUN16:27;
A17: Pg0 is continuous by A1, A2, A3, Th19;
A18: ( Pg0 | K is bounded & Pg0 is_integrable_on K ) by A1, A2, A3, A15, Th24;
then A19: ( Pg0 is_integrable_on L-Meas & integral (Pg0,K) = Integral (L-Meas,Pg0) ) by A10, A16, MESFUN14:49;
R_EAL Pg0 = ProjPMap1 (|.(R_EAL g).|,[xx1,yy1]) by MESFUNC5:def 7;
then (Integral2 (L-Meas,|.(R_EAL g).|)) . [xx1,yy1] = integral (Pg0,K) by A19, MESFUN12:def 8;
then A20: G . u1 = integral (Pg0,K) by A4, A14, FUNCT_1:49;
reconsider xx2 = x2, yy2 = y2 as Element of REAL by XREAL_0:def 1;
reconsider u2 = [xx2,yy2] as Element of [:REAL,REAL:] ;
reconsider Pg1 = ProjPMap1 (|.(R_EAL g).|,u2) as PartFunc of REAL,REAL by MESFUN16:30;
A21: dom Pg1 = K by A1, A3, A14, MESFUN16:27;
A22: Pg1 is continuous by A1, A2, A3, Th19;
A23: ( Pg1 | K is bounded & Pg1 is_integrable_on K ) by A1, A2, A3, A15, Th24;
then A24: ( Pg1 is_integrable_on L-Meas & integral (Pg1,K) = Integral (L-Meas,Pg1) ) by A10, A21, MESFUN14:49;
R_EAL Pg1 = ProjPMap1 (|.(R_EAL g).|,[xx2,yy2]) by MESFUNC5:def 7;
then (Integral2 (L-Meas,|.(R_EAL g).|)) . [xx2,yy2] = integral (Pg1,K) by A24, MESFUN12:def 8;
then G . u2 = integral (Pg1,K) by A4, A14, FUNCT_1:49;
then A25: |.((G . u2) - (G . u1)).| = |.(integral ((Pg1 - Pg0),K)).| by A21, A23, A16, A18, A20, INTEGRA6:11;
A26: dom (Pg1 - Pg0) = (dom Pg1) /\ (dom Pg0) by VALUED_1:12;
then A27: ( (Pg1 - Pg0) | K is bounded & Pg1 - Pg0 is_integrable_on K ) by A16, A17, A21, A22, INTEGRA5:10, INTEGRA5:11;
for y being Real st y in K holds
|.((Pg1 - Pg0) . y).| <= e

proof

let y be Real; :: thesis: ( y in K implies |.((Pg1 - Pg0) . y).| <= e )
assume A28: y in K ; :: thesis: |.((Pg1 - Pg0) . y).| <= e
then A29: |.(((ProjPMap1 (|.(R_EAL g).|,u2)) . y) - ((ProjPMap1 (|.(R_EAL g).|,u1)) . y)).| < e by A13, A14;
A30: - ((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;
then ((ProjPMap1 (|.(R_EAL g).|,u2)) . y) - ((ProjPMap1 (|.(R_EAL g).|,u1)) . y) = (Pg1 . y) + (- (Pg0 . y)) by A30, XXREAL_3:def 2
.= (Pg1 . y) - (Pg0 . y)
.= (Pg1 - Pg0) . y by A16, A21, A26, A28, VALUED_1:13 ;
hence |.((Pg1 - Pg0) . y).| <= e by A29, EXTREAL1:12; :: thesis: verum

end;

then |.(integral ((Pg1 - Pg0),s,t)).| <= e * (t - s) by A7, A8, A9, A16, A21, A26, A27, INTEGRA6:23;
hence |.((G . [x2,y2]) - (G . [x1,y1])).| < e by A8, A12, A11, A25, INTEGRA5:def 4; :: 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
|.((G . [y1,b₆]) - (G . [x2,y2])).| < r ) )

then A31: s < t by A7, XXREAL_0:1;
set e1 = e / 2;
A32: ( 0 < e / 2 & e / 2 < e ) by A11, XREAL_1:215, XREAL_1:216;
A33: 0 < t - s by A31, XREAL_1:50;
then consider r being Real such that
A34: ( 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, Th30, XREAL_1:139, A32;
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
|.((G . [x2,y2]) - (G . [x1,y1])).| < e ) )
thus 0 < r by A34; :: 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
|.((G . [x2,y2]) - (G . [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 |.((G . [x2,y2]) - (G . [x1,y1])).| < e )
assume A35: ( [x1,y1] in [:I,J:] & [x2,y2] in [:I,J:] & |.(x2 - x1).| < r & |.(y2 - y1).| < r ) ; :: thesis: |.((G . [x2,y2]) - (G . [x1,y1])).| < e
A36: ( x1 in I & x2 in I & y1 in J & y2 in J ) by A35, ZFMISC_1:87;
reconsider xx1 = x1, yy1 = y1 as Element of REAL by XREAL_0:def 1;
reconsider u1 = [xx1,yy1] as Element of [:REAL,REAL:] ;
reconsider Pg0 = ProjPMap1 (|.(R_EAL g).|,u1) as PartFunc of REAL,REAL by MESFUN16:30;
A37: dom Pg0 = K by A1, A3, A35, MESFUN16:27;
A38: Pg0 is continuous by A1, A2, A3, Th19;
A39: ( Pg0 | K is bounded & Pg0 is_integrable_on K ) by A1, A2, A3, A36, Th24;
then A40: ( Pg0 is_integrable_on L-Meas & integral (Pg0,K) = Integral (L-Meas,Pg0) ) by A10, A37, MESFUN14:49;
R_EAL Pg0 = ProjPMap1 (|.(R_EAL g).|,[xx1,yy1]) by MESFUNC5:def 7;
then (Integral2 (L-Meas,|.(R_EAL g).|)) . [xx1,yy1] = integral (Pg0,K) by A40, MESFUN12:def 8;
then A41: G . u1 = integral (Pg0,K) by A4, A35, FUNCT_1:49;
reconsider xx2 = x2, yy2 = y2 as Element of REAL by XREAL_0:def 1;
reconsider u2 = [xx2,yy2] as Element of [:REAL,REAL:] ;
reconsider Pg1 = ProjPMap1 (|.(R_EAL g).|,u2) as PartFunc of REAL,REAL by MESFUN16:30;
A42: dom Pg1 = K by A1, A3, A35, MESFUN16:27;
A43: Pg1 is continuous by A1, A2, A3, Th19;
A44: ( Pg1 | K is bounded & Pg1 is_integrable_on K ) by A1, A2, A3, A36, Th24;
then A45: ( Pg1 is_integrable_on L-Meas & integral (Pg1,K) = Integral (L-Meas,Pg1) ) by A10, A42, MESFUN14:49;
R_EAL Pg1 = ProjPMap1 (|.(R_EAL g).|,[xx2,yy2]) by MESFUNC5:def 7;
then (Integral2 (L-Meas,|.(R_EAL g).|)) . [xx2,yy2] = integral (Pg1,K) by A45, MESFUN12:def 8;
then G . u2 = integral (Pg1,K) by A4, A35, FUNCT_1:49;
then A46: |.((G . u2) - (G . u1)).| = |.(integral ((Pg1 - Pg0),K)).| by A42, A44, A37, A39, A41, INTEGRA6:11;
A47: dom (Pg1 - Pg0) = (dom Pg1) /\ (dom Pg0) by VALUED_1:12;
then A48: ( (Pg1 - Pg0) | K is bounded & Pg1 - Pg0 is_integrable_on K ) by A37, A38, A42, A43, INTEGRA5:10, INTEGRA5:11;
A49: ( s in ['s,t'] & t in ['s,t'] ) by A6, A7, A8;
for y being Real st y in K holds
|.((Pg1 - Pg0) . y).| <= (e / 2) / (t - s)

proof

let y be Real; :: thesis: ( y in K implies |.((Pg1 - Pg0) . y).| <= (e / 2) / (t - s) )
assume A50: y in K ; :: thesis: |.((Pg1 - Pg0) . y).| <= (e / 2) / (t - s)
A51: |.(((ProjPMap1 (|.(R_EAL g).|,u2)) . y) - ((ProjPMap1 (|.(R_EAL g).|,u1)) . y)).| < (e / 2) / (t - s) by A34, A35, A50;
A52: - ((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 A52, XXREAL_3:def 2
.= (Pg1 . y) - (Pg0 . y)
.= (Pg1 - Pg0) . y by A37, A42, A47, A50, VALUED_1:13 ;
hence |.((Pg1 - Pg0) . y).| <= (e / 2) / (t - s) by A51, EXTREAL1:12; :: thesis: verum

end;

then |.(integral ((Pg1 - Pg0),s,t)).| <= ((e / 2) / (t - s)) * (t - s) by A7, A8, A37, A42, A47, A48, A49, INTEGRA6:23;
then |.(integral ((Pg1 - Pg0),K)).| <= ((e / 2) / (t - s)) * (t - s) by A6, A8, XXREAL_1:29, INTEGRA5:def 4;
then |.(integral ((Pg1 - Pg0),K)).| <= e / 2 by A33, XCMPLX_1:87;
hence |.((G . [x2,y2]) - (G . [x1,y1])).| < e by A32, A46, XXREAL_0:2; :: thesis: verum

end;

end;

end;

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