let n be non zero Nat; :: thesis:
let D be n -element FinSequence; :: thesis:
let J be closed_interval Subset of REAL; :: thesis:
let f be PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real; :: thesis:
let g be PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL; :: thesis:
let G1 be PartFunc of REAL,REAL; :: thesis:
assume that
A1: for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL and
A2: [:(CarProduct D),J:] = dom f and
A3: f is_continuous_on [:(CarProduct D),J:] and
A4: f = g and
A5: G1 = (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) | J ; :: thesis:
set I = CarProduct D;
A6: 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 Point of (CarProduct ((Seg n) --> RNS_Real)) st x in CarProduct D holds
|.((g . [x,y2]) - (g . [x,y1])).| < e ) )

proof

let e be Real; :: thesis:
assume 0 < e ; :: thesis:
then consider r being Real such that
A7: ( 0 < r & ( for x1, x2 being Point of (CarProduct ((Seg n) --> RNS_Real))
for y1, y2 being Real st [x1,y1] in [:(CarProduct D),J:] & [x2,y2] in [:(CarProduct D),J:] & ||.(x2 - x1).|| < r & |.(y2 - y1).| < r holds
|.((g . [x2,y2]) - (g . [x1,y1])).| < e ) ) by A3, A4, A1, Th37;
take r ; :: thesis:
thus 0 < r by A7; :: thesis:
let y1, y2 be Real; :: thesis:
assume A8: ( |.(y2 - y1).| < r & y1 in J & y2 in J ) ; :: thesis:
let x be Point of (CarProduct ((Seg n) --> RNS_Real)); :: thesis:
assume x in CarProduct D ; :: thesis:
then A9: ( [x,y1] in [:(CarProduct D),J:] & [x,y2] in [:(CarProduct D),J:] ) by A8, ZFMISC_1:87;
x - x = 0. (CarProduct ((Seg n) --> RNS_Real)) by RLVECT_1:15;
then ||.(x - x).|| < r by A7;
hence |.((g . [x,y2]) - (g . [x,y1])).| < e by A7, A8, A9; :: thesis:

end;

set Rg = R_EAL g;
A10: dom (R_EAL g) = [:(CarProduct D),J:] by A2, A4, MESFUNC5:def 7;
A11: for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for y1, y2 being Element of REAL st |.(y2 - y1).| < r & y1 in J & y2 in J holds
for x being Element of CarProduct ((Seg n) --> REAL) st x in CarProduct D holds
|.(((ProjPMap2 ((R_EAL g),y2)) . x) - ((ProjPMap2 ((R_EAL g),y1)) . x)).| < e ) )

proof

let e be Real; :: thesis:
assume 0 < e ; :: thesis:
then consider r being Real such that
A12: ( 0 < r & ( for y1, y2 being Real st |.(y2 - y1).| < r & y1 in J & y2 in J holds
for x being Point of (CarProduct ((Seg n) --> RNS_Real)) st x in CarProduct D holds
|.((g . [x,y2]) - (g . [x,y1])).| < e ) ) by A6;
take r ; :: thesis:
thus 0 < r by A12; :: thesis:
let y1, y2 be Element of REAL ; :: thesis:
assume A13: ( |.(y2 - y1).| < r & y1 in J & y2 in J ) ; :: thesis:
let x be Element of CarProduct ((Seg n) --> REAL); :: thesis:
assume A14: x in CarProduct D ; :: thesis:
x is Point of (CarProduct ((Seg n) --> RNS_Real)) by MEASUR15:42;
then A15: |.((g . [x,y2]) - (g . [x,y1])).| < e by A12, A13, A14;
( (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 A13, A14, A10, ZFMISC_1:87, MESFUN12:def 4, MESFUNC5:def 7;
then ((ProjPMap2 ((R_EAL g),y2)) . x) - ((ProjPMap2 ((R_EAL g),y1)) . x) = (g . [x,y2]) - (g . [x,y1]) by Lm2;
hence |.(((ProjPMap2 ((R_EAL g),y2)) . x) - ((ProjPMap2 ((R_EAL g),y1)) . x)).| < e by A15, EXTREAL1:12; :: thesis:

end;

set T = Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g));
A16: dom (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) = REAL by FUNCT_2:def 1;
for y0, r being Real st y0 in J & 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Real st y1 in J & |.(y1 - y0).| < s holds
|.((G1 . y1) - (G1 . y0)).| < r ) )

proof

let yy0, r be Real; :: thesis:
assume A17: ( yy0 in J & 0 < r ) ; :: thesis:
reconsider y0 = yy0 as Element of REAL by XREAL_0:def 1;
reconsider RPg0 = ProjPMap2 ((R_EAL g),y0) as PartFunc of (CarProduct ((Seg n) --> REAL)),REAL by MESFUN16:30;
reconsider Pg0 = RPg0 as PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real by MEASUR15:42;
for i being Nat st i in Seg n holds
D . i is Subset of REAL by A1;
then A18: CarProduct D is Subset of (CarProduct ((Seg n) --> REAL)) by FINSEQ_1:3, Th11;
then A19: dom Pg0 = CarProduct D by A17, A2, A4, MESFUN16:28;
A20: RPg0 is_integrable_on Prod_Measure (L-Meas n) by A1, A19, A2, A3, A4, Th24, Th43;
A21: R_EAL RPg0 = ProjPMap2 ((R_EAL g),y0) by MESFUNC5:def 7;
RPg0 = ProjPMap2 ((R_EAL g),y0) ;
then A22: (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) . y0 = Integral ((Prod_Measure (L-Meas n)),(ProjPMap2 ((R_EAL g),y0))) by A1, A17, A2, A3, A4, Th45;
consider r0 being Real, E1 being Element of Prod_Field (L-Field n) such that
A23: ( E1 = CarProduct D & (Prod_Measure (L-Meas n)) . E1 = r0 & 0 <= r0 ) by A1, Th52;

per cases ;

suppose A24: r0 = 0 ; :: thesis:

consider s being Real such that
A25: ( 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 CarProduct ((Seg n) --> REAL) st x in CarProduct D holds
|.(((ProjPMap2 ((R_EAL g),y2)) . x) - ((ProjPMap2 ((R_EAL g),y1)) . x)).| < r ) ) by A11, A17;
for y1 being Real st y1 in J & |.(y1 - y0).| < s holds
|.((G1 . y1) - (G1 . yy0)).| < r

proof

proof

let x be Element of CarProduct ((Seg n) --> REAL); :: thesis:
assume A36: x in E1 ; :: thesis:
then A37: |.(((ProjPMap2 ((R_EAL g),y1)) . x) - ((ProjPMap2 ((R_EAL g),y0)) . x)).| < r by A23, A25, A26, A17;
((ProjPMap2 ((R_EAL g),y1)) . x) - ((ProjPMap2 ((R_EAL g),y0)) . x) = (RPg1 . x) - (RPg0 . x) by Lm2;
then ((ProjPMap2 ((R_EAL g),y1)) . x) - ((ProjPMap2 ((R_EAL g),y0)) . x) = (RPg1 - RPg0) . x by A23, A32, A36, VALUED_1:13;
then |.((RPg1 - RPg0) . x).| <= r by A37, EXTREAL1:12;
then ( - r <= (RPg1 - RPg0) . x & (RPg1 - RPg0) . x <= r ) by ABSVALUE:5;
hence ( - r <= (R_EAL (RPg1 - RPg0)) . x & (R_EAL (RPg1 - RPg0)) . x <= r ) by MESFUNC5:def 7; :: thesis:

end;

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

end;

suppose A44: r0 <> 0 ; :: thesis:

set r1 = r / 2;
A45: ( 0 < r / 2 & r / 2 < r ) by A17, XREAL_1:215, XREAL_1:216;
then consider s being Real such that
A46: ( 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 CarProduct ((Seg n) --> REAL) st x in CarProduct D holds
|.(((ProjPMap2 ((R_EAL g),y2)) . x) - ((ProjPMap2 ((R_EAL g),y1)) . x)).| < (r / 2) / r0 ) ) by A11, A23, A44, XREAL_1:139;
take s ; :: thesis:
thus 0 < s by A46; :: thesis:
let yy1 be Real; :: thesis:
assume A47: ( yy1 in J & |.(yy1 - yy0).| < s ) ; :: thesis:
reconsider y1 = yy1 as Element of REAL by XREAL_0:def 1;
reconsider RPg1 = ProjPMap2 ((R_EAL g),y1) as PartFunc of (CarProduct ((Seg n) --> REAL)),REAL by MESFUN16:30;
reconsider Pg1 = RPg1 as PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real by MEASUR15:42;
A48: dom Pg1 = CarProduct D by A18, A47, A2, A4, MESFUN16:28;
then A49: RPg1 is_integrable_on Prod_Measure (L-Meas n) by A1, A2, A3, A4, Th24, Th43;
A50: R_EAL RPg1 = ProjPMap2 ((R_EAL g),y1) by MESFUNC5:def 7;
RPg1 = ProjPMap2 ((R_EAL g),y1) ;
then (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) . y1 = Integral ((Prod_Measure (L-Meas n)),(ProjPMap2 ((R_EAL g),y1))) by A1, A47, A2, A3, A4, Th45;
then A51: ( G1 . yy0 = Integral ((Prod_Measure (L-Meas n)),RPg0) & G1 . yy1 = Integral ((Prod_Measure (L-Meas n)),RPg1) ) by A21, A50, A5, A17, A22, A47, FUNCT_1:49;
A52: - (G1 . yy0) = - (Integral ((Prod_Measure (L-Meas n)),RPg0)) by A51, XXREAL_3:def 3;
A53: RPg1 - RPg0 is_integrable_on Prod_Measure (L-Meas n) by A20, A49, MESFUN6C:34;
A54: dom (RPg1 - RPg0) = (CarProduct D) /\ (CarProduct D) by A19, A48, VALUED_1:12;
then A55: dom (R_EAL (RPg1 - RPg0)) = E1 by A23, MESFUNC5:def 7;
A56: (Prod_Measure (L-Meas n)) . E1 < +infty by A23, XREAL_0:def 1, XXREAL_0:9;
for x being Element of CarProduct ((Seg n) --> REAL) st x in E1 holds
( - ((r / 2) / r0) <= (R_EAL (RPg1 - RPg0)) . x & (R_EAL (RPg1 - RPg0)) . x <= (r / 2) / r0 )

proof

let x be Element of CarProduct ((Seg n) --> REAL); :: thesis:
assume A57: x in E1 ; :: thesis:
then A58: |.(((ProjPMap2 ((R_EAL g),y1)) . x) - ((ProjPMap2 ((R_EAL g),y0)) . x)).| < (r / 2) / r0 by A23, A46, A47, A17;
((ProjPMap2 ((R_EAL g),y1)) . x) - ((ProjPMap2 ((R_EAL g),y0)) . x) = (RPg1 . x) - (RPg0 . x) by Lm2;
then ((ProjPMap2 ((R_EAL g),y1)) . x) - ((ProjPMap2 ((R_EAL g),y0)) . x) = (RPg1 - RPg0) . x by A23, A54, A57, VALUED_1:13;
then |.((RPg1 - RPg0) . x).| <= (r / 2) / r0 by A58, EXTREAL1:12;
then ( - ((r / 2) / r0) <= (RPg1 - RPg0) . x & (RPg1 - RPg0) . x <= (r / 2) / r0 ) by ABSVALUE:5;
hence ( - ((r / 2) / r0) <= (R_EAL (RPg1 - RPg0)) . x & (R_EAL (RPg1 - RPg0)) . x <= (r / 2) / r0 ) by MESFUNC5:def 7; :: thesis:

end;

end;

then G1 | J is continuous by A5, A16, FCONT_1:14;
hence G1 is continuous by A5; :: thesis: