let n be non zero Nat; :: thesis: for D being n -element FinSequence
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 G1 being PartFunc of REAL,REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & [:(CarProduct D),J:] = dom f & f is_continuous_on [:(CarProduct D),J:] & f = g & G1 = (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) | J holds
G1 is continuous
let D be n -element FinSequence; :: 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 G1 being PartFunc of REAL,REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & [:(CarProduct D),J:] = dom f & f is_continuous_on [:(CarProduct D),J:] & f = g & G1 = (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) | J holds
G1 is continuous
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 G1 being PartFunc of REAL,REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & [:(CarProduct D),J:] = dom f & f is_continuous_on [:(CarProduct D),J:] & f = g & G1 = (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) | J holds
G1 is continuous
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 G1 being PartFunc of REAL,REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & [:(CarProduct D),J:] = dom f & f is_continuous_on [:(CarProduct D),J:] & f = g & G1 = (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) | J holds
G1 is continuous
let g be PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL; :: thesis: for G1 being PartFunc of REAL,REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & [:(CarProduct D),J:] = dom f & f is_continuous_on [:(CarProduct D),J:] & f = g & G1 = (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) | J holds
G1 is continuous
let G1 be PartFunc of REAL,REAL; :: thesis: ( ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & [:(CarProduct D),J:] = dom f & f is_continuous_on [:(CarProduct D),J:] & f = g & G1 = (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) | J implies G1 is continuous )
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: G1 is continuous
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: ( 0 < e implies 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 ) ) )
assume 0 < e ; :: thesis: 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 ) )
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 A1, A3, A4, Th39;
take r ; :: thesis: ( 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 ) )
thus 0 < r by A7; :: thesis: 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
let y1, y2 be Real; :: thesis: ( |.(y2 - y1).| < r & y1 in J & y2 in J implies for x being Point of (CarProduct ((Seg n) --> RNS_Real)) st x in CarProduct D holds
|.((|.g.| . [x,y2]) - (|.g.| . [x,y1])).| < e )
assume A8: ( |.(y2 - y1).| < r & y1 in J & y2 in J ) ; :: thesis: for x being Point of (CarProduct ((Seg n) --> RNS_Real)) st x in CarProduct D holds
|.((|.g.| . [x,y2]) - (|.g.| . [x,y1])).| < e
let x be Point of (CarProduct ((Seg n) --> RNS_Real)); :: thesis: ( x in CarProduct D implies |.((|.g.| . [x,y2]) - (|.g.| . [x,y1])).| < e )
assume x in CarProduct D ; :: thesis: |.((|.g.| . [x,y2]) - (|.g.| . [x,y1])).| < e
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: verum

end;

set Rg = R_EAL g;
dom |.(R_EAL g).| = dom (R_EAL g) by MESFUNC1:def 10;
then A10: dom |.(R_EAL g).| = [:(CarProduct D),J:] by A2, A4, MESFUNC5:def 7;
A11: for x being Element of CarProduct ((Seg n) --> REAL)
for y being Element of REAL st x in CarProduct D & y in J holds
( (ProjPMap2 (|.(R_EAL g).|,y)) . x = |.(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 CarProduct D & y in J holds
( (ProjPMap2 (|.(R_EAL g).|,y)) . x = |.(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 CarProduct D & y in J implies ( (ProjPMap2 (|.(R_EAL g).|,y)) . x = |.(R_EAL g).| . (x,y) & |.(R_EAL g).| . (x,y) = |.(g . [x,y]).| & |.(R_EAL g).| . (x,y) = |.g.| . [x,y] ) )
assume A12: ( x in CarProduct D & y in J ) ; :: thesis: ( (ProjPMap2 (|.(R_EAL g).|,y)) . x = |.(R_EAL g).| . (x,y) & |.(R_EAL g).| . (x,y) = |.(g . [x,y]).| & |.(R_EAL g).| . (x,y) = |.g.| . [x,y] )
hence (ProjPMap2 (|.(R_EAL g).|,y)) . x = |.(R_EAL g).| . (x,y) by A10, ZFMISC_1:87, MESFUN12:def 4; :: thesis: ( |.(R_EAL g).| . (x,y) = |.(g . [x,y]).| & |.(R_EAL g).| . (x,y) = |.g.| . [x,y] )
[x,y] in dom g by A12, A2, A4, ZFMISC_1:87;
then A13: [x,y] in dom |.g.| by VALUED_1:def 11;
A14: (R_EAL g) . [x,y] = g . [x,y] by MESFUNC5:def 7;
|.(R_EAL g).| . (x,y) = |.((R_EAL g) . [x,y]).| by A12, A10, ZFMISC_1:87, MESFUNC1:def 10;
hence |.(R_EAL g).| . (x,y) = |.(g . [x,y]).| by A14, 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, A13; :: thesis: verum

end;

A15: 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: ( 0 < e implies 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 ) ) )
assume 0 < e ; :: thesis: 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 ) )
then consider r being Real such that
A16: ( 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: ( 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 ) )
thus 0 < r by A16; :: thesis: 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
let y1, y2 be Element of REAL ; :: thesis: ( |.(y2 - y1).| < r & y1 in J & y2 in J implies 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 )
assume A17: ( |.(y2 - y1).| < r & y1 in J & y2 in J ) ; :: thesis: 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
let x be Element of CarProduct ((Seg n) --> REAL); :: thesis: ( x in CarProduct D implies |.(((ProjPMap2 (|.(R_EAL g).|,y2)) . x) - ((ProjPMap2 (|.(R_EAL g).|,y1)) . x)).| < e )
assume A18: x in CarProduct D ; :: thesis: |.(((ProjPMap2 (|.(R_EAL g).|,y2)) . x) - ((ProjPMap2 (|.(R_EAL g).|,y1)) . x)).| < e
x is Point of (CarProduct ((Seg n) --> RNS_Real)) by MEASUR15:42;
then A19: |.((|.g.| . [x,y2]) - (|.g.| . [x,y1])).| < e by A16, A17, A18;
( (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 A11, A17, A18;
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 A19, EXTREAL1:12; :: thesis: verum

end;

set T = Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|);
A20: 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: ( yy0 in J & 0 < r implies ex s being Real st
( 0 < s & ( for y1 being Real st y1 in J & |.(y1 - yy0).| < s holds
|.((G1 . y1) - (G1 . yy0)).| < r ) ) )
assume A21: ( yy0 in J & 0 < r ) ; :: thesis: ex s being Real st
( 0 < s & ( for y1 being Real st y1 in J & |.(y1 - yy0).| < s holds
|.((G1 . y1) - (G1 . yy0)).| < r ) )
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 A22: CarProduct D is Subset of (CarProduct ((Seg n) --> REAL)) by FINSEQ_1:3, Th11;
then A23: dom Pg0 = CarProduct D by A21, A2, A4, MESFUN16:28;
A24: RPg0 is_integrable_on Prod_Measure (L-Meas n) by A1, A23, A2, A3, A4, Th26, Th43;
A25: R_EAL RPg0 = ProjPMap2 (|.(R_EAL g).|,y0) by MESFUNC5:def 7;
RPg0 = ProjPMap2 (|.(R_EAL g).|,y0) ;
then A26: (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) . y0 = Integral ((Prod_Measure (L-Meas n)),(ProjPMap2 (|.(R_EAL g).|,y0))) by A1, A21, A2, A3, A4, Th48;
consider r0 being Real, E1 being Element of Prod_Field (L-Field n) such that
A27: ( E1 = CarProduct D & (Prod_Measure (L-Meas n)) . E1 = r0 & 0 <= r0 ) by A1, Th52;

per cases ( r0 = 0 or r0 <> 0 ) ;

suppose A28: r0 = 0 ; :: thesis: ex s being Real st
( 0 < s & ( for y1 being Real st y1 in J & |.(y1 - yy0).| < s holds
|.((G1 . y1) - (G1 . yy0)).| < r ) )

consider s being Real such that
A29: ( 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 A15, A21;
for y1 being Real st y1 in J & |.(y1 - y0).| < s holds
|.((G1 . y1) - (G1 . yy0)).| < r

proof

let yy1 be Real; :: thesis: ( yy1 in J & |.(yy1 - y0).| < s implies |.((G1 . yy1) - (G1 . yy0)).| < r )
assume A30: ( yy1 in J & |.(yy1 - y0).| < s ) ; :: thesis: |.((G1 . yy1) - (G1 . yy0)).| < r
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;
A31: dom Pg1 = CarProduct D by A22, A30, A2, A4, MESFUN16:28;
A32: 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, A30, A2, A3, A4, Th48;
then A33: ( G1 . yy0 = Integral ((Prod_Measure (L-Meas n)),RPg0) & G1 . yy1 = Integral ((Prod_Measure (L-Meas n)),RPg1) ) by A25, A32, A5, A21, A26, A30, FUNCT_1:49;
A34: - (G1 . yy0) = - (Integral ((Prod_Measure (L-Meas n)),RPg0)) by A33, XXREAL_3:def 3;
A35: RPg1 is_integrable_on Prod_Measure (L-Meas n) by A1, A31, A2, A3, A4, Th26, Th43;
then A36: RPg1 - RPg0 is_integrable_on Prod_Measure (L-Meas n) by A24, MESFUN6C:34;
A37: dom (RPg1 - RPg0) = (CarProduct D) /\ (CarProduct D) by A23, A31, VALUED_1:12;
then A38: dom (R_EAL (RPg1 - RPg0)) = E1 by A27, MESFUNC5:def 7;
A39: (Prod_Measure (L-Meas n)) . E1 < +infty by A27, XREAL_0:def 1, XXREAL_0:9;
for x being Element of CarProduct ((Seg n) --> REAL) st x in E1 holds
( - r <= (R_EAL (RPg1 - RPg0)) . x & (R_EAL (RPg1 - RPg0)) . x <= r )

proof

let x be Element of CarProduct ((Seg n) --> REAL); :: thesis: ( x in E1 implies ( - r <= (R_EAL (RPg1 - RPg0)) . x & (R_EAL (RPg1 - RPg0)) . x <= r ) )
assume A40: x in E1 ; :: thesis: ( - r <= (R_EAL (RPg1 - RPg0)) . x & (R_EAL (RPg1 - RPg0)) . x <= r )
then A41: |.(((ProjPMap2 (|.(R_EAL g).|,y1)) . x) - ((ProjPMap2 (|.(R_EAL g).|,y0)) . x)).| < r by A27, A29, A30, A21;
((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 A27, A37, A40, VALUED_1:13;
then |.((RPg1 - RPg0) . x).| <= r by A41, 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: verum

end;

then ( (- r) * ((Prod_Measure (L-Meas n)) . E1) <= Integral ((Prod_Measure (L-Meas n)),((R_EAL (RPg1 - RPg0)) | E1)) & Integral ((Prod_Measure (L-Meas n)),((R_EAL (RPg1 - RPg0)) | E1)) <= r * ((Prod_Measure (L-Meas n)) . E1) ) by A38, A36, A39, MESFUNC7:26;
then A42: ( 0 <= Integral ((Prod_Measure (L-Meas n)),(R_EAL (RPg1 - RPg0))) & Integral ((Prod_Measure (L-Meas n)),(R_EAL (RPg1 - RPg0))) <= 0 ) by A28, A27, A38;
A43: (- 1) (#) RPg0 = - RPg0 by VALUED_1:def 6;
A44: ( (- 1) (#) RPg0 is_integrable_on Prod_Measure (L-Meas n) & Integral ((Prod_Measure (L-Meas n)),((- 1) (#) RPg0)) = (- 1) * (Integral ((Prod_Measure (L-Meas n)),RPg0)) ) by A24, MESFUNC6:102;
then A45: ( - RPg0 is_integrable_on Prod_Measure (L-Meas n) & Integral ((Prod_Measure (L-Meas n)),(- RPg0)) = - (Integral ((Prod_Measure (L-Meas n)),RPg0)) ) by A43, XXREAL_3:91;
A46: dom (- RPg0) = E1 by A27, A23, A43, VALUED_1:def 5;
A47: RPg1 + (- RPg0) = RPg1 - RPg0 by VALUED_1:def 9;
ex E being Element of Prod_Field (L-Field n) st
( E = (dom RPg1) /\ (dom (- RPg0)) & Integral ((Prod_Measure (L-Meas n)),(RPg1 + (- RPg0))) = (Integral ((Prod_Measure (L-Meas n)),(RPg1 | E))) + (Integral ((Prod_Measure (L-Meas n)),((- RPg0) | E))) ) by A35, A43, A44, MESFUNC6:101;
then Integral ((Prod_Measure (L-Meas n)),(RPg1 - RPg0)) = (G1 . yy1) + (- (G1 . yy0)) by A33, A34, A27, A31, A46, A47, A45, XXREAL_3:def 2;
hence |.((G1 . yy1) - (G1 . yy0)).| < r by A21, A42; :: thesis: verum

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 A29; :: thesis: verum

end;

suppose A48: r0 <> 0 ; :: thesis: ex s being Real st
( 0 < s & ( for y1 being Real st y1 in J & |.(y1 - yy0).| < s holds
|.((G1 . y1) - (G1 . yy0)).| < r ) )

set r1 = r / 2;
A49: ( 0 < r / 2 & r / 2 < r ) by A21, XREAL_1:215, XREAL_1:216;
then consider s being Real such that
A50: ( 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 A15, A48, A27, XREAL_1:139;
take s ; :: thesis: ( 0 < s & ( for y1 being Real st y1 in J & |.(y1 - yy0).| < s holds
|.((G1 . y1) - (G1 . yy0)).| < r ) )
thus 0 < s by A50; :: thesis: for y1 being Real st y1 in J & |.(y1 - yy0).| < s holds
|.((G1 . y1) - (G1 . yy0)).| < r
let yy1 be Real; :: thesis: ( yy1 in J & |.(yy1 - yy0).| < s implies |.((G1 . yy1) - (G1 . yy0)).| < r )
assume A51: ( yy1 in J & |.(yy1 - yy0).| < s ) ; :: thesis: |.((G1 . yy1) - (G1 . yy0)).| < r
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;
A52: dom Pg1 = CarProduct D by A22, A51, A2, A4, MESFUN16:28;
then A53: RPg1 is_integrable_on Prod_Measure (L-Meas n) by A1, A2, A3, A4, Th26, Th43;
A54: 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, A51, A2, A3, A4, Th48;
then A55: ( G1 . yy0 = Integral ((Prod_Measure (L-Meas n)),RPg0) & G1 . yy1 = Integral ((Prod_Measure (L-Meas n)),RPg1) ) by A25, A54, A5, A21, A26, A51, FUNCT_1:49;
A56: - (G1 . yy0) = - (Integral ((Prod_Measure (L-Meas n)),RPg0)) by A55, XXREAL_3:def 3;
A57: RPg1 - RPg0 is_integrable_on Prod_Measure (L-Meas n) by A24, A53, MESFUN6C:34;
A58: dom (RPg1 - RPg0) = (CarProduct D) /\ (CarProduct D) by A23, A52, VALUED_1:12;
then A59: dom (R_EAL (RPg1 - RPg0)) = E1 by A27, MESFUNC5:def 7;
A60: (Prod_Measure (L-Meas n)) . E1 < +infty by A27, XXREAL_0:9, XREAL_0:def 1;
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: ( x in E1 implies ( - ((r / 2) / r0) <= (R_EAL (RPg1 - RPg0)) . x & (R_EAL (RPg1 - RPg0)) . x <= (r / 2) / r0 ) )
assume A61: x in E1 ; :: thesis: ( - ((r / 2) / r0) <= (R_EAL (RPg1 - RPg0)) . x & (R_EAL (RPg1 - RPg0)) . x <= (r / 2) / r0 )
then A62: |.(((ProjPMap2 (|.(R_EAL g).|,y1)) . x) - ((ProjPMap2 (|.(R_EAL g).|,y0)) . x)).| < (r / 2) / r0 by A27, A50, A51, A21;
((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 A27, A58, A61, VALUED_1:13;
then |.((RPg1 - RPg0) . x).| <= (r / 2) / r0 by A62, 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: verum

end;

then A63: ( (- ((r / 2) / r0)) * ((Prod_Measure (L-Meas n)) . E1) <= Integral ((Prod_Measure (L-Meas n)),((R_EAL (RPg1 - RPg0)) | E1)) & Integral ((Prod_Measure (L-Meas n)),((R_EAL (RPg1 - RPg0)) | E1)) <= ((r / 2) / r0) * ((Prod_Measure (L-Meas n)) . E1) ) by A59, A57, A60, MESFUNC7:26;
A64: (- ((r / 2) / r0)) * r0 = - (((r / 2) / r0) * r0) ;
((r / 2) / r0) * r0 = r / 2 by A48, XCMPLX_1:87;
then A65: ( - (r / 2) <= Integral ((Prod_Measure (L-Meas n)),(R_EAL (RPg1 - RPg0))) & Integral ((Prod_Measure (L-Meas n)),(R_EAL (RPg1 - RPg0))) <= r / 2 ) by A63, A64, A59, A27, XXREAL_3:def 5;
A66: (- 1) (#) RPg0 = - RPg0 by VALUED_1:def 6;
A67: ( (- 1) (#) RPg0 is_integrable_on Prod_Measure (L-Meas n) & Integral ((Prod_Measure (L-Meas n)),((- 1) (#) RPg0)) = (- 1) * (Integral ((Prod_Measure (L-Meas n)),RPg0)) ) by A24, MESFUNC6:102;
then A68: ( - RPg0 is_integrable_on Prod_Measure (L-Meas n) & Integral ((Prod_Measure (L-Meas n)),(- RPg0)) = - (Integral ((Prod_Measure (L-Meas n)),RPg0)) ) by A66, XXREAL_3:91;
A69: dom (- RPg0) = E1 by A27, A23, A66, VALUED_1:def 5;
A70: RPg1 + (- RPg0) = RPg1 - RPg0 by VALUED_1:def 9;
ex E being Element of Prod_Field (L-Field n) st
( E = (dom RPg1) /\ (dom (- RPg0)) & Integral ((Prod_Measure (L-Meas n)),(RPg1 + (- RPg0))) = (Integral ((Prod_Measure (L-Meas n)),(RPg1 | E))) + (Integral ((Prod_Measure (L-Meas n)),((- RPg0) | E))) ) by A53, A66, A67, MESFUNC6:101;
then Integral ((Prod_Measure (L-Meas n)),(RPg1 - RPg0)) = (G1 . yy1) + (- (G1 . yy0)) by A27, A52, A69, A70, A55, A56, A68, XXREAL_3:def 2;
then |.((G1 . yy1) - (G1 . yy0)).| <= r / 2 by A65, ABSVALUE:5;
hence |.((G1 . yy1) - (G1 . yy0)).| < r by XXREAL_0:2, A49; :: thesis: verum

end;

end;

end;

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