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;
set Rg = R_EAL g;
dom |.(R_EAL g).| = dom (R_EAL g) by MESFUNC1:def 10;
then A8: dom |.(R_EAL g).| = [:I,J:] by A3, A5, MESFUNC5:def 7;
A9: for x being Element of CarProduct ((Seg n) --> REAL)
for y being Element of REAL st x in I & y in J holds
( (ProjPMap1 (|.(R_EAL g).|,x)) . y = |.(R_EAL g).| . (x,y) & |.(R_EAL g).| . (x,y) = |.(g . [x,y]).| & |.(R_EAL g).| . (x,y) = |.g.| . [x,y] )

proof

let x be Element of CarProduct ((Seg n) --> REAL); :: thesis: for y being Element of REAL st x in I & y in J holds
( (ProjPMap1 (|.(R_EAL g).|,x)) . y = |.(R_EAL g).| . (x,y) & |.(R_EAL g).| . (x,y) = |.(g . [x,y]).| & |.(R_EAL g).| . (x,y) = |.g.| . [x,y] )
let y be Element of REAL ; :: thesis: ( x in I & y in J implies ( (ProjPMap1 (|.(R_EAL g).|,x)) . y = |.(R_EAL g).| . (x,y) & |.(R_EAL g).| . (x,y) = |.(g . [x,y]).| & |.(R_EAL g).| . (x,y) = |.g.| . [x,y] ) )
assume A10: ( x in I & y in J ) ; :: thesis: ( (ProjPMap1 (|.(R_EAL g).|,x)) . y = |.(R_EAL g).| . (x,y) & |.(R_EAL g).| . (x,y) = |.(g . [x,y]).| & |.(R_EAL g).| . (x,y) = |.g.| . [x,y] )
hence (ProjPMap1 (|.(R_EAL g).|,x)) . y = |.(R_EAL g).| . (x,y) by A8, ZFMISC_1:87, MESFUN12:def 3; :: thesis: ( |.(R_EAL g).| . (x,y) = |.(g . [x,y]).| & |.(R_EAL g).| . (x,y) = |.g.| . [x,y] )
[x,y] in dom g by A10, A3, A5, ZFMISC_1:87;
then A11: [x,y] in dom |.g.| by VALUED_1:def 11;
A12: (R_EAL g) . [x,y] = g . [x,y] by MESFUNC5:def 7;
|.(R_EAL g).| . (x,y) = |.((R_EAL g) . [x,y]).| by A10, A8, ZFMISC_1:87, MESFUNC1:def 10;
hence |.(R_EAL g).| . (x,y) = |.(g . [x,y]).| by A12, EXTREAL1:12; :: thesis: |.(R_EAL g).| . (x,y) = |.g.| . [x,y]
hence |.(R_EAL g).| . (x,y) = |.g.| . [x,y] by VALUED_1:def 11, A11; :: thesis: verum

end;

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 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, Th39;

A15: now :: 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 A16: ( ||.(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

hereby :: thesis: verum

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 A17: ( [x1,y] in [:I,J:] & [x2,y] in [:I,J:] ) by A16, ZFMISC_1:87;
|.(y - y).| < r by A14;
hence |.((|.g.| . [x2,y]) - (|.g.| . [x1,y])).| < e by A14, A16, A17; :: thesis: verum

end;

end;

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
A18: ( xx1 = x1 & xx2 = x2 ) and
A19: ( ||.(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 A20: y in J ; :: thesis: |.(((ProjPMap1 (|.(R_EAL g).|,x2)) . y) - ((ProjPMap1 (|.(R_EAL g).|,x1)) . y)).| < e
then A21: |.((|.g.| . [x2,y]) - (|.g.| . [x1,y])).| < e by A15, A18, A19;
( (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 A9, A19, A20;
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 A21, EXTREAL1:12; :: thesis: verum

end;

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

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

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

then A25: ( c in J & d in J ) by A7;
then reconsider J = J as non empty closed_interval Subset of REAL ;
A26: 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 A27: ( 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;
A28: dom Pg0 = J by A27, A2, A22, A3, A5, MESFUN16:27;
A29: Pg0 | (dom Pg0) is continuous by A3, A4, A5, Th25;
A30: ( Pg0 | J is bounded & Pg0 is_integrable_on J ) by A27, A3, A4, A5, A2, A22, Th28;
A31: (Integral2 (L-Meas,|.(R_EAL g).|)) . x0 = integral (Pg0,J) by A27, A3, A4, A5, A2, A22, Th32;

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

suppose A32: 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
A33: ( 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, A27;
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 A34: ( 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;
A35: dom Pg1 = J by A34, A3, A5, A2, A22, MESFUN16:27;
A36: Pg1 | (dom Pg1) is continuous by A3, A4, A5, Th25;
A37: ( Pg1 | J is bounded & Pg1 is_integrable_on J ) by A34, A3, A4, A5, A2, A22, Th28;
(Integral2 (L-Meas,|.(R_EAL g).|)) . x1 = integral (Pg1,J) by A34, A3, A4, A5, A2, A22, Th32;
then ( G2 . xx0 = integral (Pg0,J) & G2 . xx1 = integral (Pg1,J) ) by A6, A27, A31, A34, FUNCT_1:49;
then ( G2 . xx0 = integral (Pg0,c,d) & G2 . xx1 = integral (Pg1,c,d) ) by A7, A26, XXREAL_1:29, INTEGRA5:def 4;
then ( G2 /. xx0 = integral (Pg0,c,d) & G2 /. xx1 = integral (Pg1,c,d) ) by A2, A22, A6, A23, A27, A34, PARTFUN1:def 6;
then A38: (G2 /. xx1) - (G2 /. xx0) = (integral (Pg1,c,d)) - (integral (Pg0,c,d)) by DUALSP03:4;
A39: dom (Pg1 - Pg0) = J /\ J by A28, A35, VALUED_1:12;
then A40: ( (Pg1 - Pg0) | J is bounded & Pg1 - Pg0 is_integrable_on J ) by A29, A36, 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 A41: y in J ; :: thesis: |.((Pg1 - Pg0) . y).| <= r
then A42: |.(((ProjPMap1 (|.(R_EAL g).|,x1)) . y) - ((ProjPMap1 (|.(R_EAL g).|,x0)) . y)).| < r by A33, A34, A27;
A43: - ((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 A43, 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 A39, A41, VALUED_1:13;
hence |.((Pg1 - Pg0) . y).| <= r by A42, EXTREAL1:12; :: thesis: verum

end;

then |.(integral ((Pg1 - Pg0),c,d)).| <= r * (d - c) by A24, A26, A39, A40, A25, INTEGRA6:23;
then |.((integral (Pg1,c,d)) - (integral (Pg0,c,d))).| <= r * (d - c) by A32, A26, A35, A37, A28, A30, INTEGRA6:12;
hence ||.((G2 /. xx1) - (G2 /. xx0)).|| < r by A32, A27, A38, 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 A33; :: 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 A24, XXREAL_0:1;
then A44: 0 < d - c by XREAL_1:50;
set r1 = r / 2;
A45: ( 0 < r / 2 & r / 2 < r ) by A27, XREAL_1:215, XREAL_1:216;
consider s being Real such that
A46: ( 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, A45, A44;
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 A46; :: 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 A47: ( 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;
A48: dom Pg1 = J by A47, A3, A5, A2, A22, MESFUN16:27;
A49: Pg1 | (dom Pg1) is continuous by A3, A4, A5, Th25;
A50: ( Pg1 | J is bounded & Pg1 is_integrable_on J ) by A47, A3, A4, A5, A2, A22, Th28;
(Integral2 (L-Meas,|.(R_EAL g).|)) . x1 = integral (Pg1,J) by A47, A3, A4, A5, A2, A22, Th32;
then ( G2 . xx0 = integral (Pg0,J) & G2 . xx1 = integral (Pg1,J) ) by A6, A27, A31, A47, FUNCT_1:49;
then ( G2 . xx0 = integral (Pg0,c,d) & G2 . xx1 = integral (Pg1,c,d) ) by A7, A26, XXREAL_1:29, INTEGRA5:def 4;
then ( G2 /. xx0 = integral (Pg0,c,d) & G2 /. xx1 = integral (Pg1,c,d) ) by A2, A22, A6, A23, A27, A47, 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 A24, A26, A48, A50, A28, A30, INTEGRA6:12;
then A51: ||.((G2 /. xx1) - (G2 /. xx0)).|| = |.(integral ((Pg1 - Pg0),c,d)).| by EUCLID:def 2;
A52: dom (Pg1 - Pg0) = J /\ J by A28, A48, VALUED_1:12;
then A53: ( (Pg1 - Pg0) | J is bounded & Pg1 - Pg0 is_integrable_on J ) by A29, A49, 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 A54: y in J ; :: thesis: |.((Pg1 - Pg0) . y).| <= (r / 2) / (d - c)
then A55: |.(((ProjPMap1 (|.(R_EAL g).|,x1)) . y) - ((ProjPMap1 (|.(R_EAL g).|,x0)) . y)).| < (r / 2) / (d - c) by A46, A47, A27;
A56: - ((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 A56, 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 A52, A54, VALUED_1:13;
hence |.((Pg1 - Pg0) . y).| <= (r / 2) / (d - c) by A55, EXTREAL1:12; :: thesis: verum

end;

then |.(integral ((Pg1 - Pg0),c,d)).| <= ((r / 2) / (d - c)) * (d - c) by A24, A26, A52, A53, A25, INTEGRA6:23;
then |.(integral ((Pg1 - Pg0),c,d)).| <= r / 2 by A44, XCMPLX_1:87;
hence ||.((G2 /. xx1) - (G2 /. xx0)).|| < r by A51, XXREAL_0:2, A45; :: thesis: verum

end;

end;

end;

hence G2 is_continuous_on I by A2, A22, A6, A23, NFCONT_1:19; :: thesis: verum

end;

suppose A57: 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 A58: ( 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 A2, A3, A5, A22, A58, MESFUN16:27;
then Integral (L-Meas,(ProjPMap1 (|.(R_EAL g).|,x0))) = 0 by A57, A7, XXREAL_1:29, MESFUN16:1;
then A59: (Integral2 (L-Meas,|.(R_EAL g).|)) . x0 = 0 by MESFUN12:def 8;
consider s being Real such that
A60: ( 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, A58;
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 A61: ( 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 A3, A5, A2, A22, A61, MESFUN16:27;
then Integral (L-Meas,(ProjPMap1 (|.(R_EAL g).|,x1))) = 0 by A57, 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, A58, A59, A61, FUNCT_1:49;
then ( G2 /. xx0 = 0 & G2 /. xx1 = 0 ) by A2, A6, A22, A23, A58, A61, PARTFUN1:def 6;
then (G2 /. xx1) - (G2 /. xx0) = 0. RNS_Real by RLVECT_1:15;
hence ||.((G2 /. xx1) - (G2 /. xx0)).|| < r by A58; :: 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 A60; :: thesis: verum

end;

hence G2 is_continuous_on I by A2, A6, A22, A23, NFCONT_1:19; :: thesis: verum

end;

end;