let n be non zero Nat; :: thesis: for D being n -element FinSequence
for I being Subset of (CarProduct ((Seg n) --> RNS_Real))
for J being closed_interval Subset of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for G2 being PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & I = CarProduct D & [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G2 = (Integral2 (L-Meas,(R_EAL g))) | I holds
G2 is_continuous_on I
let D be n -element FinSequence; :: thesis: for I being Subset of (CarProduct ((Seg n) --> RNS_Real))
for J being closed_interval Subset of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for G2 being PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & I = CarProduct D & [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G2 = (Integral2 (L-Meas,(R_EAL g))) | I holds
G2 is_continuous_on I
let I be Subset of (CarProduct ((Seg n) --> RNS_Real)); :: thesis: for J being closed_interval Subset of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for G2 being PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & I = CarProduct D & [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G2 = (Integral2 (L-Meas,(R_EAL g))) | I holds
G2 is_continuous_on I
let J be closed_interval Subset of REAL; :: thesis: for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for G2 being PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & I = CarProduct D & [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G2 = (Integral2 (L-Meas,(R_EAL g))) | I holds
G2 is_continuous_on I
let f be PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for G2 being PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & I = CarProduct D & [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G2 = (Integral2 (L-Meas,(R_EAL g))) | I holds
G2 is_continuous_on I
let g be PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL; :: thesis: for G2 being PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & I = CarProduct D & [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G2 = (Integral2 (L-Meas,(R_EAL g))) | I holds
G2 is_continuous_on I
let G2 be PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real; :: thesis: ( ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & I = CarProduct D & [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G2 = (Integral2 (L-Meas,(R_EAL g))) | I implies G2 is_continuous_on I )
assume that
A1: for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL and
A2: I = CarProduct D and
A3: [:I,J:] = dom f and
A4: f is_continuous_on [:I,J:] and
A5: f = g and
A6: G2 = (Integral2 (L-Meas,(R_EAL g))) | I ; :: thesis: G2 is_continuous_on I
consider c, d being Real such that
A7: J = [.c,d.] by MEASURE5:def 3;
A8: for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2 being Point of (CarProduct ((Seg n) --> RNS_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 Point of (CarProduct ((Seg n) --> RNS_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 Point of (CarProduct ((Seg n) --> RNS_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
A9: ( 0 < r & ( for x1, x2 being Point of (CarProduct ((Seg n) --> RNS_Real))
for 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 A1, A2, A4, A5, Th37;
take r ; :: thesis: ( 0 < r & ( for x1, x2 being Point of (CarProduct ((Seg n) --> RNS_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 A9; :: thesis: for x1, x2 being Point of (CarProduct ((Seg n) --> RNS_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 Point of (CarProduct ((Seg n) --> RNS_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 A10: ( ||.(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 A11: ( [x1,y] in [:I,J:] & [x2,y] in [:I,J:] ) by A10, ZFMISC_1:87;
|.(y - y).| < r by A9;
hence |.((g . [x2,y]) - (g . [x1,y])).| < e by A9, A10, A11; :: thesis: verum

end;

set Rg = R_EAL g;
A12: dom (R_EAL g) = [:I,J:] by A3, A5, MESFUNC5:def 7;
A13: for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2 being Element of CarProduct ((Seg n) --> REAL)
for xx1, xx2 being Point of (CarProduct ((Seg n) --> RNS_Real)) st xx1 = x1 & xx2 = x2 & ||.(xx2 - xx1).|| < 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 CarProduct ((Seg n) --> REAL)
for xx1, xx2 being Point of (CarProduct ((Seg n) --> RNS_Real)) st xx1 = x1 & xx2 = x2 & ||.(xx2 - xx1).|| < 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 CarProduct ((Seg n) --> REAL)
for xx1, xx2 being Point of (CarProduct ((Seg n) --> RNS_Real)) st xx1 = x1 & xx2 = x2 & ||.(xx2 - xx1).|| < 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
A14: ( 0 < r & ( for xx1, xx2 being Point of (CarProduct ((Seg n) --> RNS_Real)) st ||.(xx2 - xx1).|| < r & xx1 in I & xx2 in I holds
for y being Real st y in J holds
|.((g . [xx2,y]) - (g . [xx1,y])).| < e ) ) by A8;
take r ; :: thesis: ( 0 < r & ( for x1, x2 being Element of CarProduct ((Seg n) --> REAL)
for xx1, xx2 being Point of (CarProduct ((Seg n) --> RNS_Real)) st xx1 = x1 & xx2 = x2 & ||.(xx2 - xx1).|| < 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 A14; :: thesis: for x1, x2 being Element of CarProduct ((Seg n) --> REAL)
for xx1, xx2 being Point of (CarProduct ((Seg n) --> RNS_Real)) st xx1 = x1 & xx2 = x2 & ||.(xx2 - xx1).|| < 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 CarProduct ((Seg n) --> REAL); :: thesis: for xx1, xx2 being Point of (CarProduct ((Seg n) --> RNS_Real)) st xx1 = x1 & xx2 = x2 & ||.(xx2 - xx1).|| < 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 xx1, xx2 be Point of (CarProduct ((Seg n) --> RNS_Real)); :: thesis: ( xx1 = x1 & xx2 = x2 & ||.(xx2 - xx1).|| < 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 that
A15: ( xx1 = x1 & xx2 = x2 ) and
A16: ( ||.(xx2 - xx1).|| < 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 A17: y in J ; :: thesis: |.(((ProjPMap1 ((R_EAL g),x2)) . y) - ((ProjPMap1 ((R_EAL g),x1)) . y)).| < e
then A18: |.((g . [x2,y]) - (g . [x1,y])).| < e by A14, A15, A16;
( (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 A12, A16, A17, ZFMISC_1:87, MESFUN12:def 3, MESFUNC5:def 7;
then ((ProjPMap1 ((R_EAL g),x2)) . y) - ((ProjPMap1 ((R_EAL g),x1)) . y) = (g . [x2,y]) - (g . [x1,y]) by Lm2;
hence |.(((ProjPMap1 ((R_EAL g),x2)) . y) - ((ProjPMap1 ((R_EAL g),x1)) . y)).| < e by A18, EXTREAL1:12; :: thesis: verum

end;

set F = Integral2 (L-Meas,(R_EAL g));
A19: dom (Integral2 (L-Meas,(R_EAL g))) = CarProduct ((Seg n) --> REAL) by FUNCT_2:def 1;
for i being Nat st i in Seg n holds
D . i is Subset of REAL by A1;
then A20: CarProduct D is Subset of (CarProduct ((Seg n) --> REAL)) by FINSEQ_1:3, Th11;

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

suppose A21: c <= d ; :: thesis: G2 is_continuous_on I

then A22: ( c in J & d in J ) by A7;
then reconsider J = J as non empty closed_interval Subset of REAL ;
A23: J = ['c,d'] by A7, XXREAL_1:29, INTEGRA5:def 3;
for x0 being Point of (CarProduct ((Seg n) --> RNS_Real))
for r being Real st x0 in I & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of (CarProduct ((Seg n) --> RNS_Real)) st x1 in I & ||.(x1 - x0).|| < s holds
||.((G2 /. x1) - (G2 /. x0)).|| < r ) )

proof

let xx0 be Point of (CarProduct ((Seg n) --> RNS_Real)); :: thesis: for r being Real st xx0 in I & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of (CarProduct ((Seg n) --> RNS_Real)) st x1 in I & ||.(x1 - xx0).|| < s holds
||.((G2 /. x1) - (G2 /. xx0)).|| < r ) )
let r be Real; :: thesis: ( xx0 in I & 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Point of (CarProduct ((Seg n) --> RNS_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 Point of (CarProduct ((Seg n) --> RNS_Real)) st x1 in I & ||.(x1 - xx0).|| < s holds
||.((G2 /. x1) - (G2 /. xx0)).|| < r ) )
reconsider x0 = xx0 as Element of CarProduct ((Seg n) --> REAL) by MEASUR15:42;
reconsider Pg0 = ProjPMap1 ((R_EAL g),x0) as PartFunc of REAL,REAL by MESFUN16:30;
A25: dom Pg0 = J by A24, A2, A20, A3, A5, MESFUN16:27;
A26: Pg0 is continuous by A3, A4, A5, Th23;
A27: ( Pg0 | J is bounded & Pg0 is_integrable_on J ) by A24, A3, A4, A5, A2, A20, Th27;
A28: (Integral2 (L-Meas,(R_EAL g))) . x0 = integral (Pg0,J) by A24, A3, A4, A5, A2, A20, Th30;

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

suppose A29: c = d ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Point of (CarProduct ((Seg n) --> RNS_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 CarProduct ((Seg n) --> REAL)
for xx1, xx2 being Point of (CarProduct ((Seg n) --> RNS_Real)) st xx1 = x1 & xx2 = x2 & ||.(xx2 - xx1).|| < 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 A13, A24;
for x1 being Point of (CarProduct ((Seg n) --> RNS_Real)) st x1 in I & ||.(x1 - xx0).|| < s holds
||.((G2 /. x1) - (G2 /. xx0)).|| < r

proof

let xx1 be Point of (CarProduct ((Seg n) --> RNS_Real)); :: thesis: ( xx1 in I & ||.(xx1 - xx0).|| < s implies ||.((G2 /. xx1) - (G2 /. xx0)).|| < r )
assume A31: ( xx1 in I & ||.(xx1 - xx0).|| < s ) ; :: thesis: ||.((G2 /. xx1) - (G2 /. xx0)).|| < r
reconsider x1 = xx1 as Element of CarProduct ((Seg n) --> REAL) by MEASUR15:42;
reconsider Pg1 = ProjPMap1 ((R_EAL g),x1) as PartFunc of REAL,REAL by MESFUN16:30;
A32: dom Pg1 = J by A31, A3, A5, A2, A20, MESFUN16:27;
A33: Pg1 is continuous by A3, A4, A5, Th23;
A34: ( Pg1 | J is bounded & Pg1 is_integrable_on J ) by A31, A3, A4, A5, A2, A20, Th27;
(Integral2 (L-Meas,(R_EAL g))) . x1 = integral (Pg1,J) by A31, A3, A4, A5, A2, A20, Th30;
then ( G2 . xx0 = integral (Pg0,J) & G2 . xx1 = integral (Pg1,J) ) by A6, A24, A28, A31, FUNCT_1:49;
then ( G2 . xx0 = integral (Pg0,c,d) & G2 . xx1 = integral (Pg1,c,d) ) by A7, A23, XXREAL_1:29, INTEGRA5:def 4;
then ( G2 /. xx0 = integral (Pg0,c,d) & G2 /. xx1 = integral (Pg1,c,d) ) by A2, A6, A19, A20, A24, A31, PARTFUN1:def 6;
then A35: (G2 /. xx1) - (G2 /. xx0) = (integral (Pg1,c,d)) - (integral (Pg0,c,d)) by DUALSP03: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 A21, A23, A36, A37, A22, INTEGRA6:23;
then |.((integral (Pg1,c,d)) - (integral (Pg0,c,d))).| < r by A29, A24, A23, A32, A34, A25, A27, INTEGRA6:12;
hence ||.((G2 /. xx1) - (G2 /. xx0)).|| < r by A35, EUCLID:def 2; :: thesis: verum

end;

hence ex s being Real st
( 0 < s & ( for x1 being Point of (CarProduct ((Seg n) --> RNS_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 Point of (CarProduct ((Seg n) --> RNS_Real)) st x1 in I & ||.(x1 - xx0).|| < s holds
||.((G2 /. x1) - (G2 /. xx0)).|| < r ) )

then c < d by A21, 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 CarProduct ((Seg n) --> REAL)
for xx1, xx2 being Point of (CarProduct ((Seg n) --> RNS_Real)) st xx1 = x1 & xx2 = x2 & ||.(xx2 - xx1).|| < 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 A13, XREAL_1:139, A42, A41;
take s ; :: thesis: ( 0 < s & ( for x1 being Point of (CarProduct ((Seg n) --> RNS_Real)) st x1 in I & ||.(x1 - xx0).|| < s holds
||.((G2 /. x1) - (G2 /. xx0)).|| < r ) )
thus 0 < s by A43; :: thesis: for x1 being Point of (CarProduct ((Seg n) --> RNS_Real)) st x1 in I & ||.(x1 - xx0).|| < s holds
||.((G2 /. x1) - (G2 /. xx0)).|| < r
let xx1 be Point of (CarProduct ((Seg n) --> RNS_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 CarProduct ((Seg n) --> REAL) by MEASUR15:42;
reconsider Pg1 = ProjPMap1 ((R_EAL g),x1) as PartFunc of REAL,REAL by MESFUN16:30;
A45: dom Pg1 = J by A44, A3, A5, A2, A20, MESFUN16:27;
A46: Pg1 is continuous by A3, A4, A5, Th23;
A47: ( Pg1 | J is bounded & Pg1 is_integrable_on J ) by A44, A3, A4, A5, A2, A20, Th27;
(Integral2 (L-Meas,(R_EAL g))) . x1 = integral (Pg1,J) by A44, A3, A4, A5, A2, A20, Th30;
then ( G2 . xx0 = integral (Pg0,J) & G2 . xx1 = integral (Pg1,J) ) by A6, A24, A28, A44, FUNCT_1:49;
then ( G2 . xx0 = integral (Pg0,c,d) & G2 . xx1 = integral (Pg1,c,d) ) by A7, A23, XXREAL_1:29, INTEGRA5:def 4;
then ( G2 /. xx0 = integral (Pg0,c,d) & G2 /. xx1 = integral (Pg1,c,d) ) by A2, A6, A19, A20, A24, A44, PARTFUN1:def 6;
then (G2 /. xx1) - (G2 /. xx0) = (integral (Pg1,c,d)) - (integral (Pg0,c,d)) by DUALSP03:4;
then (G2 /. xx1) - (G2 /. xx0) = integral ((Pg1 - Pg0),c,d) by A21, A23, A45, A47, A25, A27, INTEGRA6:12;
then A48: ||.((G2 /. xx1) - (G2 /. xx0)).|| = |.(integral ((Pg1 - Pg0),c,d)).| by EUCLID:def 2;
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 A21, A23, A49, A50, A22, 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;

hence G2 is_continuous_on I by A2, A6, A19, A20, NFCONT_1:19; :: thesis: verum

end;

suppose A54: c > d ; :: thesis: G2 is_continuous_on I

for x0 being Point of (CarProduct ((Seg n) --> RNS_Real))
for r being Real st x0 in I & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of (CarProduct ((Seg n) --> RNS_Real)) st x1 in I & ||.(x1 - x0).|| < s holds
||.((G2 /. x1) - (G2 /. x0)).|| < r ) )

proof

let xx0 be Point of (CarProduct ((Seg n) --> RNS_Real)); :: thesis: for r being Real st xx0 in I & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of (CarProduct ((Seg n) --> RNS_Real)) st x1 in I & ||.(x1 - xx0).|| < s holds
||.((G2 /. x1) - (G2 /. xx0)).|| < r ) )
let r be Real; :: thesis: ( xx0 in I & 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Point of (CarProduct ((Seg n) --> RNS_Real)) st x1 in I & ||.(x1 - xx0).|| < s holds
||.((G2 /. x1) - (G2 /. xx0)).|| < r ) ) )
assume A55: ( xx0 in I & 0 < r ) ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Point of (CarProduct ((Seg n) --> RNS_Real)) st x1 in I & ||.(x1 - xx0).|| < s holds
||.((G2 /. x1) - (G2 /. xx0)).|| < r ) )
reconsider x0 = xx0 as Element of CarProduct ((Seg n) --> REAL) by MEASUR15:42;
reconsider Pg0 = ProjPMap1 ((R_EAL g),x0) as PartFunc of REAL,REAL by MESFUN16:30;
dom Pg0 = J by A55, A2, A20, A3, A5, MESFUN16:27;
then Integral (L-Meas,(ProjPMap1 ((R_EAL g),x0))) = 0 by A54, A7, XXREAL_1:29, MESFUN16:1;
then A56: (Integral2 (L-Meas,(R_EAL g))) . x0 = 0 by MESFUN12:def 8;
consider s being Real such that
A57: ( 0 < s & ( for x1, x2 being Element of CarProduct ((Seg n) --> REAL)
for xx1, xx2 being Point of (CarProduct ((Seg n) --> RNS_Real)) st xx1 = x1 & xx2 = x2 & ||.(xx2 - xx1).|| < 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 A13, A55;
for x1 being Point of (CarProduct ((Seg n) --> RNS_Real)) st x1 in I & ||.(x1 - xx0).|| < s holds
||.((G2 /. x1) - (G2 /. xx0)).|| < r

proof

let xx1 be Point of (CarProduct ((Seg n) --> RNS_Real)); :: thesis: ( xx1 in I & ||.(xx1 - xx0).|| < s implies ||.((G2 /. xx1) - (G2 /. xx0)).|| < r )
assume A58: ( xx1 in I & ||.(xx1 - xx0).|| < s ) ; :: thesis: ||.((G2 /. xx1) - (G2 /. xx0)).|| < r
reconsider x1 = xx1 as Element of CarProduct ((Seg n) --> REAL) by MEASUR15:42;
reconsider Pg1 = ProjPMap1 ((R_EAL g),x1) as PartFunc of REAL,REAL by MESFUN16:30;
dom Pg1 = J by A58, A3, A5, A2, A20, MESFUN16:27;
then Integral (L-Meas,(ProjPMap1 ((R_EAL g),x1))) = 0 by A54, A7, XXREAL_1:29, MESFUN16:1;
then (Integral2 (L-Meas,(R_EAL g))) . x1 = 0 by MESFUN12:def 8;
then ( G2 . xx0 = 0 & G2 . xx1 = 0 ) by A6, A55, A56, A58, FUNCT_1:49;
then ( G2 /. xx0 = 0 & G2 /. xx1 = 0 ) by A2, A6, A19, A20, A55, A58, PARTFUN1:def 6;
then (G2 /. xx1) - (G2 /. xx0) = 0. RNS_Real by RLVECT_1:15;
hence ||.((G2 /. xx1) - (G2 /. xx0)).|| < r by A55; :: thesis: verum

end;

hence ex s being Real st
( 0 < s & ( for x1 being Point of (CarProduct ((Seg n) --> RNS_Real)) st x1 in I & ||.(x1 - xx0).|| < s holds
||.((G2 /. x1) - (G2 /. xx0)).|| < r ) ) by A57; :: thesis: verum

end;

hence G2 is_continuous_on I by A2, A6, A19, A20, NFCONT_1:19; :: thesis: verum

end;

end;