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 Gxy being PartFunc of REAL,REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & Gxy = (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) | K holds
Gxy is continuous
let f be PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for Gxy being PartFunc of REAL,REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & Gxy = (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) | K holds
Gxy is continuous
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis: for Gxy being PartFunc of REAL,REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & Gxy = (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) | K holds
Gxy is continuous
let Gxy be PartFunc of REAL,REAL; :: thesis: ( [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & Gxy = (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) | K implies Gxy is continuous )
assume that
A1: [:[:I,J:],K:] = dom f and
A2: f is_continuous_on [:[:I,J:],K:] and
A3: f = g and
A4: Gxy = (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) | K ; :: thesis: Gxy is continuous
consider a, b being Real such that
A5: I = [.a,b.] by MEASURE5:def 3;
A6: a <= b by A5, XXREAL_1:29;
then A7: ( a in I & b in I ) by A5;
A8: [.a,b.] = ['a,b'] by A5, XXREAL_1:29, INTEGRA5:def 3;
consider c, d being Real such that
A9: J = [.c,d.] by MEASURE5:def 3;
A10: c <= d by A9, XXREAL_1:29;
then A11: ( c in J & d in J ) by A9;
A12: [.c,d.] = ['c,d'] by A9, XXREAL_1:29, INTEGRA5:def 3;
A13: for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for z1, z2 being Real st |.(z2 - z1).| < r & z1 in K & z2 in K holds
for x, y being Real st x in I & y in J holds
|.((g . [x,y,z2]) - (g . [x,y,z1])).| < e ) )

proof

let e be Real; :: thesis: ( 0 < e implies ex r being Real st
( 0 < r & ( for z1, z2 being Real st |.(z2 - z1).| < r & z1 in K & z2 in K holds
for x, y being Real st x in I & y in J holds
|.((g . [x,y,z2]) - (g . [x,y,z1])).| < e ) ) )
assume 0 < e ; :: thesis: ex r being Real st
( 0 < r & ( for z1, z2 being Real st |.(z2 - z1).| < r & z1 in K & z2 in K holds
for x, y being Real st x in I & y in J holds
|.((g . [x,y,z2]) - (g . [x,y,z1])).| < e ) )
then consider r being Real such that
A14: ( 0 < r & ( for x1, x2, y1, y2, z1, z2 being Real st x1 in I & x2 in I & y1 in J & y2 in J & z1 in K & z2 in K & |.(x2 - x1).| < r & |.(y2 - y1).| < r & |.(z2 - z1).| < r holds
|.((g . [x2,y2,z2]) - (g . [x1,y1,z1])).| < e ) ) by A2, A3, Th8;
take r ; :: thesis: ( 0 < r & ( for z1, z2 being Real st |.(z2 - z1).| < r & z1 in K & z2 in K holds
for x, y being Real st x in I & y in J holds
|.((g . [x,y,z2]) - (g . [x,y,z1])).| < e ) )
thus 0 < r by A14; :: thesis: for z1, z2 being Real st |.(z2 - z1).| < r & z1 in K & z2 in K holds
for x, y being Real st x in I & y in J holds
|.((g . [x,y,z2]) - (g . [x,y,z1])).| < e
let z1, z2 be Real; :: thesis: ( |.(z2 - z1).| < r & z1 in K & z2 in K implies for x, y being Real st x in I & y in J holds
|.((g . [x,y,z2]) - (g . [x,y,z1])).| < e )
assume A15: ( |.(z2 - z1).| < r & z1 in K & z2 in K ) ; :: thesis: for x, y being Real st x in I & y in J holds
|.((g . [x,y,z2]) - (g . [x,y,z1])).| < e
let x, y be Real; :: thesis: ( x in I & y in J implies |.((g . [x,y,z2]) - (g . [x,y,z1])).| < e )
assume A16: ( x in I & y in J ) ; :: thesis: |.((g . [x,y,z2]) - (g . [x,y,z1])).| < e
( |.(x - x).| < r & |.(y - y).| < r ) by A14;
hence |.((g . [x,y,z2]) - (g . [x,y,z1])).| < e by A14, A15, A16; :: thesis: verum

end;

set Rg = R_EAL g;
A17: dom (R_EAL g) = [:[:I,J:],K:] by A1, A3, MESFUNC5:def 7;
A18: for x, y, z being Element of REAL st x in I & y in J & z in K holds
( (ProjPMap2 ((R_EAL g),z)) . (x,y) = (R_EAL g) . ([x,y],z) & (R_EAL g) . ([x,y],z) = g . [x,y,z] & (R_EAL g) . ([x,y],z) = g . [x,y,z] )

proof

let x, y, z be Element of REAL ; :: thesis: ( x in I & y in J & z in K implies ( (ProjPMap2 ((R_EAL g),z)) . (x,y) = (R_EAL g) . ([x,y],z) & (R_EAL g) . ([x,y],z) = g . [x,y,z] & (R_EAL g) . ([x,y],z) = g . [x,y,z] ) )
assume A19: ( x in I & y in J & z in K ) ; :: thesis: ( (ProjPMap2 ((R_EAL g),z)) . (x,y) = (R_EAL g) . ([x,y],z) & (R_EAL g) . ([x,y],z) = g . [x,y,z] & (R_EAL g) . ([x,y],z) = g . [x,y,z] )
then [x,y] in [:I,J:] by ZFMISC_1:87;
hence (ProjPMap2 ((R_EAL g),z)) . (x,y) = (R_EAL g) . ([x,y],z) by A17, A19, ZFMISC_1:87, MESFUN12:def 4; :: thesis: ( (R_EAL g) . ([x,y],z) = g . [x,y,z] & (R_EAL g) . ([x,y],z) = g . [x,y,z] )
thus (R_EAL g) . ([x,y],z) = g . [x,y,z] by MESFUNC5:def 7; :: thesis: (R_EAL g) . ([x,y],z) = g . [x,y,z]
thus (R_EAL g) . ([x,y],z) = g . [x,y,z] by MESFUNC5:def 7; :: thesis: verum

end;

A20: for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for z1, z2 being Element of REAL st |.(z2 - z1).| < r & z1 in K & z2 in K holds
for x, y being Element of REAL st x in I & y in J holds
|.(((ProjPMap1 ((ProjPMap2 ((R_EAL g),z2)),x)) . y) - ((ProjPMap1 ((ProjPMap2 ((R_EAL g),z1)),x)) . y)).| < e ) )

proof

let e be Real; :: thesis: ( 0 < e implies ex r being Real st
( 0 < r & ( for z1, z2 being Element of REAL st |.(z2 - z1).| < r & z1 in K & z2 in K holds
for x, y being Element of REAL st x in I & y in J holds
|.(((ProjPMap1 ((ProjPMap2 ((R_EAL g),z2)),x)) . y) - ((ProjPMap1 ((ProjPMap2 ((R_EAL g),z1)),x)) . y)).| < e ) ) )
assume 0 < e ; :: thesis: ex r being Real st
( 0 < r & ( for z1, z2 being Element of REAL st |.(z2 - z1).| < r & z1 in K & z2 in K holds
for x, y being Element of REAL st x in I & y in J holds
|.(((ProjPMap1 ((ProjPMap2 ((R_EAL g),z2)),x)) . y) - ((ProjPMap1 ((ProjPMap2 ((R_EAL g),z1)),x)) . y)).| < e ) )
then consider r being Real such that
A21: ( 0 < r & ( for z1, z2 being Real st |.(z2 - z1).| < r & z1 in K & z2 in K holds
for x, y being Real st x in I & y in J holds
|.((g . [x,y,z2]) - (g . [x,y,z1])).| < e ) ) by A13;
take r ; :: thesis: ( 0 < r & ( for z1, z2 being Element of REAL st |.(z2 - z1).| < r & z1 in K & z2 in K holds
for x, y being Element of REAL st x in I & y in J holds
|.(((ProjPMap1 ((ProjPMap2 ((R_EAL g),z2)),x)) . y) - ((ProjPMap1 ((ProjPMap2 ((R_EAL g),z1)),x)) . y)).| < e ) )
thus 0 < r by A21; :: thesis: for z1, z2 being Element of REAL st |.(z2 - z1).| < r & z1 in K & z2 in K holds
for x, y being Element of REAL st x in I & y in J holds
|.(((ProjPMap1 ((ProjPMap2 ((R_EAL g),z2)),x)) . y) - ((ProjPMap1 ((ProjPMap2 ((R_EAL g),z1)),x)) . y)).| < e
let z1, z2 be Element of REAL ; :: thesis: ( |.(z2 - z1).| < r & z1 in K & z2 in K implies for x, y being Element of REAL st x in I & y in J holds
|.(((ProjPMap1 ((ProjPMap2 ((R_EAL g),z2)),x)) . y) - ((ProjPMap1 ((ProjPMap2 ((R_EAL g),z1)),x)) . y)).| < e )
assume A22: ( |.(z2 - z1).| < r & z1 in K & z2 in K ) ; :: thesis: for x, y being Element of REAL st x in I & y in J holds
|.(((ProjPMap1 ((ProjPMap2 ((R_EAL g),z2)),x)) . y) - ((ProjPMap1 ((ProjPMap2 ((R_EAL g),z1)),x)) . y)).| < e
let x, y be Element of REAL ; :: thesis: ( x in I & y in J implies |.(((ProjPMap1 ((ProjPMap2 ((R_EAL g),z2)),x)) . y) - ((ProjPMap1 ((ProjPMap2 ((R_EAL g),z1)),x)) . y)).| < e )
assume A23: ( x in I & y in J ) ; :: thesis: |.(((ProjPMap1 ((ProjPMap2 ((R_EAL g),z2)),x)) . y) - ((ProjPMap1 ((ProjPMap2 ((R_EAL g),z1)),x)) . y)).| < e
then A24: |.((g . [x,y,z2]) - (g . [x,y,z1])).| < e by A21, A22;
a24: (g . [x,y,z2]) - (g . [x,y,z1]) = (g . [x,y,z2]) - (g . [x,y,z1]) ;
dom (ProjPMap2 ((R_EAL g),z1)) = [:I,J:] by A22, A1, A3, MESFUN16:28;
then A25: (ProjPMap1 ((ProjPMap2 ((R_EAL g),z1)),x)) . y = (ProjPMap2 ((R_EAL g),z1)) . (x,y) by A23, ZFMISC_1:87, MESFUN12:def 3;
dom (ProjPMap2 ((R_EAL g),z2)) = [:I,J:] by A22, A1, A3, MESFUN16:28;
then A26: (ProjPMap1 ((ProjPMap2 ((R_EAL g),z2)),x)) . y = (ProjPMap2 ((R_EAL g),z2)) . (x,y) by A23, ZFMISC_1:87, MESFUN12:def 3;
( (ProjPMap2 ((R_EAL g),z1)) . (x,y) = (R_EAL g) . ([x,y],z1) & (R_EAL g) . ([x,y],z1) = g . [x,y,z1] & (ProjPMap2 ((R_EAL g),z2)) . (x,y) = (R_EAL g) . ([x,y],z2) & (R_EAL g) . ([x,y],z2) = g . [x,y,z2] ) by A18, A22, A23;
hence |.(((ProjPMap1 ((ProjPMap2 ((R_EAL g),z2)),x)) . y) - ((ProjPMap1 ((ProjPMap2 ((R_EAL g),z1)),x)) . y)).| < e by A24, a24, A25, A26, EXTREAL1:12; :: thesis: verum

end;

A27: dom (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) = REAL by FUNCT_2:def 1;
for z0, r being Real st z0 in K & 0 < r holds
ex s being Real st
( 0 < s & ( for z1 being Real st z1 in K & |.(z1 - z0).| < s holds
|.((Gxy . z1) - (Gxy . z0)).| < r ) )

proof

let zz0, r be Real; :: thesis: ( zz0 in K & 0 < r implies ex s being Real st
( 0 < s & ( for z1 being Real st z1 in K & |.(z1 - zz0).| < s holds
|.((Gxy . z1) - (Gxy . zz0)).| < r ) ) )
assume A28: ( zz0 in K & 0 < r ) ; :: thesis: ex s being Real st
( 0 < s & ( for z1 being Real st z1 in K & |.(z1 - zz0).| < s holds
|.((Gxy . z1) - (Gxy . zz0)).| < r ) )
reconsider z0 = zz0 as Element of REAL by XREAL_0:def 1;
reconsider Pg20 = ProjPMap2 ((R_EAL g),z0) as PartFunc of [:REAL,REAL:],REAL by MESFUN16:30;
reconsider Pf20 = Pg20 as PartFunc of [:RNS_Real,RNS_Real:],RNS_Real ;
A29: dom Pg20 = [:I,J:] by A28, A1, A3, MESFUN16:28;
then A30: Pf20 is_continuous_on [:I,J:] by A1, A2, A3, Th18;
then reconsider Pg0 = (Integral2 (L-Meas,(R_EAL Pg20))) | I as PartFunc of REAL,REAL by A29, MESFUN16:51;
A31: dom (Integral2 (L-Meas,(R_EAL Pg20))) = REAL by FUNCT_2:def 1;
then A32: dom Pg0 = I ;
A33: Pg0 is continuous by A1, A2, A3, A29, Th18, MESFUN16:53;
then A34: ( Pg0 | I is bounded & Pg0 is_integrable_on I ) by A31, INTEGRA5:10, INTEGRA5:11;
(Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) . z0 = Integral ((Prod_Measure (L-Meas,L-Meas)),Pg20) by A28, A1, A2, A3, Th23
.= Integral ((Prod_Measure (L-Meas,L-Meas)),(R_EAL Pg20)) ;
then (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) . z0 = integral (Pg0,I) by A1, A2, A3, A29, Th18, MESFUN16:58;
then Gxy . zz0 = integral (Pg0,I) by A4, A28, FUNCT_1:49;
then A35: Gxy . zz0 = integral (Pg0,a,b) by A5, A8, XXREAL_1:29, INTEGRA5:def 4;

per cases ( ( a = b & c = d ) or ( a <> b & c = d ) or ( a = b & c <> d ) or ( a <> b & c <> d ) ) ;

suppose A36: ( a = b & c = d ) ; :: thesis: ex s being Real st
( 0 < s & ( for z1 being Real st z1 in K & |.(z1 - zz0).| < s holds
|.((Gxy . z1) - (Gxy . zz0)).| < r ) )

consider s being Real such that
A37: ( 0 < s & ( for z1, z2 being Element of REAL st |.(z2 - z1).| < s & z1 in K & z2 in K holds
for x, y being Element of REAL st x in I & y in J holds
|.(((ProjPMap1 ((ProjPMap2 ((R_EAL g),z2)),x)) . y) - ((ProjPMap1 ((ProjPMap2 ((R_EAL g),z1)),x)) . y)).| < r ) ) by A20, A28;
for z1 being Real st z1 in K & |.(z1 - z0).| < s holds
|.((Gxy . z1) - (Gxy . zz0)).| < r

proof

let zz1 be Real; :: thesis: ( zz1 in K & |.(zz1 - z0).| < s implies |.((Gxy . zz1) - (Gxy . zz0)).| < r )
assume A38: ( zz1 in K & |.(zz1 - z0).| < s ) ; :: thesis: |.((Gxy . zz1) - (Gxy . zz0)).| < r
reconsider z1 = zz1 as Element of REAL by XREAL_0:def 1;
reconsider Pg21 = ProjPMap2 ((R_EAL g),z1) as PartFunc of [:REAL,REAL:],REAL by MESFUN16:30;
reconsider Pf21 = Pg21 as PartFunc of [:RNS_Real,RNS_Real:],RNS_Real ;
A39: dom Pg21 = [:I,J:] by A38, A1, A3, MESFUN16:28;
then A40: Pf21 is_continuous_on [:I,J:] by A1, A2, A3, Th18;
then reconsider Pg1 = (Integral2 (L-Meas,(R_EAL Pg21))) | I as PartFunc of REAL,REAL by A39, MESFUN16:51;
A41: dom (Integral2 (L-Meas,(R_EAL Pg21))) = REAL by FUNCT_2:def 1;
then A42: dom Pg1 = I ;
A43: Pg1 is continuous by A1, A2, A3, A39, Th18, MESFUN16:53;
then A44: ( Pg1 | I is bounded & Pg1 is_integrable_on I ) by A41, INTEGRA5:10, INTEGRA5:11;
(Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) . z1 = Integral ((Prod_Measure (L-Meas,L-Meas)),Pg21) by A38, A1, A2, A3, Th23
.= Integral ((Prod_Measure (L-Meas,L-Meas)),(R_EAL Pg21)) ;
then (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) . z1 = integral (Pg1,I) by A1, A2, A3, A39, Th18, MESFUN16:58;
then Gxy . zz1 = integral (Pg1,I) by A4, A38, FUNCT_1:49;
then A45: Gxy . zz1 = integral (Pg1,a,b) by A5, A8, XXREAL_1:29, INTEGRA5:def 4;
A46: dom (Pg1 - Pg0) = I /\ I by A32, A42, VALUED_1:12;
then A47: ( Pg1 - Pg0 is_integrable_on I & (Pg1 - Pg0) | I is bounded ) by A33, A43, INTEGRA5:10, INTEGRA5:11;
for x being Element of REAL st x in I holds
|.((Pg1 - Pg0) . x).| <= r

proof

let x be Element of REAL ; :: thesis: ( x in I implies |.((Pg1 - Pg0) . x).| <= r )
assume A48: x in I ; :: thesis: |.((Pg1 - Pg0) . x).| <= r
reconsider Pg120 = ProjPMap1 (Pg20,x) as PartFunc of REAL,REAL ;
A49: dom Pg120 = J by A48, A29, MESFUN16:25;
ProjPMap1 ((R_EAL Pg20),x) = R_EAL (ProjPMap1 (Pg20,x)) by MESFUN16:31;
then A50: Pg120 = ProjPMap1 ((R_EAL Pg20),x) by MESFUNC5:def 7;
A51: Pg120 is continuous by A29, A30, MESFUN16:33;
A52: ( Pg120 | J is bounded & Pg120 is_integrable_on J ) by A29, A30, A48, A50, MESFUN16:40;
reconsider Pg121 = ProjPMap1 (Pg21,x) as PartFunc of REAL,REAL ;
A53: dom Pg121 = J by A48, A39, MESFUN16:25;
ProjPMap1 ((R_EAL Pg21),x) = R_EAL (ProjPMap1 (Pg21,x)) by MESFUN16:31;
then A54: Pg121 = ProjPMap1 ((R_EAL Pg21),x) by MESFUNC5:def 7;
A55: Pg121 is continuous by A39, A40, MESFUN16:33;
A56: ( Pg121 | J is bounded & Pg121 is_integrable_on J ) by A39, A40, A48, A54, MESFUN16:40;
Pg0 . x = (Integral2 (L-Meas,(R_EAL Pg20))) . x by A48, FUNCT_1:49;
then Pg0 . x = Integral (L-Meas,(ProjPMap1 ((R_EAL Pg20),x))) by MESFUN12:def 8;
then Pg0 . x = Integral (L-Meas,Pg120) by MESFUN16:31;
then A57: Pg0 . x = integral (Pg120,c,d) by A9, A12, A49, A52, XXREAL_1:29, MESFUN14:50;
Pg1 . x = (Integral2 (L-Meas,(R_EAL Pg21))) . x by A48, FUNCT_1:49;
then Pg1 . x = Integral (L-Meas,(ProjPMap1 ((R_EAL Pg21),x))) by MESFUN12:def 8;
then Pg1 . x = Integral (L-Meas,Pg121) by MESFUN16:31;
then Pg1 . x = integral (Pg121,c,d) by A9, A12, A53, A56, XXREAL_1:29, MESFUN14:50;
then A58: (Pg1 . x) - (Pg0 . x) = integral ((Pg121 - Pg120),c,d) by A9, A10, A12, A52, A56, A53, A49, A57, INTEGRA6:12;
A59: dom (Pg121 - Pg120) = J /\ J by A49, A53, VALUED_1:12;
then A60: ( (Pg121 - Pg120) | J is bounded & Pg121 - Pg120 is_integrable_on J ) by A51, A55, INTEGRA5:10, INTEGRA5:11;
for y being Real st y in J holds
|.((Pg121 - Pg120) . y).| <= r

proof

let y be Real; :: thesis: ( y in J implies |.((Pg121 - Pg120) . y).| <= r )
assume A61: y in J ; :: thesis: |.((Pg121 - Pg120) . y).| <= r
reconsider yy = y as Element of REAL by XREAL_0:def 1;
A62: ( Pg120 . y = (ProjPMap1 ((ProjPMap2 ((R_EAL g),z0)),x)) . yy & Pg121 . y = (ProjPMap1 ((ProjPMap2 ((R_EAL g),z1)),x)) . yy ) by A50, A54, MESFUNC5:def 7;
A63: (Pg121 - Pg120) . y = (Pg121 . y) - (Pg120 . y) by A59, A61, VALUED_1:13
.= ((ProjPMap1 ((ProjPMap2 ((R_EAL g),z1)),x)) . yy) - ((ProjPMap1 ((ProjPMap2 ((R_EAL g),z0)),x)) . yy) by A62, Lm6 ;
|.(((ProjPMap1 ((ProjPMap2 ((R_EAL g),z1)),x)) . yy) - ((ProjPMap1 ((ProjPMap2 ((R_EAL g),z0)),x)) . yy)).| < r by A28, A38, A48, A61, A37;
hence |.((Pg121 - Pg120) . y).| <= r by A63, EXTREAL1:12; :: thesis: verum

end;

then |.(integral ((Pg121 - Pg120),c,d)).| <= r * (d - c) by A9, A10, A11, A12, A59, A60, INTEGRA6:23;
hence |.((Pg1 - Pg0) . x).| <= r by A28, A36, A46, A48, A58, VALUED_1:13; :: thesis: verum

end;

then for x being Real st x in ['a,b'] holds
|.((Pg1 - Pg0) . x).| <= r by A5, A8;
then |.(integral ((Pg1 - Pg0),a,b)).| <= r * (b - a) by A5, A6, A7, A8, A46, A47, INTEGRA6:23;
hence |.((Gxy . zz1) - (Gxy . zz0)).| < r by A5, A8, A28, A32, A34, A36, A42, A44, A35, A45, INTEGRA6:12; :: thesis: verum

end;

hence ex s being Real st
( 0 < s & ( for z1 being Real st z1 in K & |.(z1 - zz0).| < s holds
|.((Gxy . z1) - (Gxy . zz0)).| < r ) ) by A37; :: thesis: verum

end;

suppose A64: ( a <> b & c = d ) ; :: thesis: ex s being Real st
( 0 < s & ( for z1 being Real st z1 in K & |.(z1 - zz0).| < s holds
|.((Gxy . z1) - (Gxy . zz0)).| < r ) )

then a < b by A6, XXREAL_0:1;
then A65: 0 < b - a by XREAL_1:50;
set r1 = r / 2;
A66: ( 0 < r / 2 & r / 2 < r ) by A28, XREAL_1:215, XREAL_1:216;
then A67: 0 < (r / 2) / (b - a) by A65, XREAL_1:139;
consider s being Real such that
A68: ( 0 < s & ( for z1, z2 being Element of REAL st |.(z2 - z1).| < s & z1 in K & z2 in K holds
for x, y being Element of REAL st x in I & y in J holds
|.(((ProjPMap1 ((ProjPMap2 ((R_EAL g),z2)),x)) . y) - ((ProjPMap1 ((ProjPMap2 ((R_EAL g),z1)),x)) . y)).| < (r / 2) / (b - a) ) ) by A20, A65, A66, XREAL_1:139;
for z1 being Real st z1 in K & |.(z1 - z0).| < s holds
|.((Gxy . z1) - (Gxy . zz0)).| < r

proof

let zz1 be Real; :: thesis: ( zz1 in K & |.(zz1 - z0).| < s implies |.((Gxy . zz1) - (Gxy . zz0)).| < r )
assume A69: ( zz1 in K & |.(zz1 - z0).| < s ) ; :: thesis: |.((Gxy . zz1) - (Gxy . zz0)).| < r
reconsider z1 = zz1 as Element of REAL by XREAL_0:def 1;
reconsider Pg21 = ProjPMap2 ((R_EAL g),z1) as PartFunc of [:REAL,REAL:],REAL by MESFUN16:30;
reconsider Pf21 = Pg21 as PartFunc of [:RNS_Real,RNS_Real:],RNS_Real ;
A70: dom Pg21 = [:I,J:] by A69, A1, A3, MESFUN16:28;
then A71: Pf21 is_continuous_on [:I,J:] by A1, A2, A3, Th18;
then reconsider Pg1 = (Integral2 (L-Meas,(R_EAL Pg21))) | I as PartFunc of REAL,REAL by A70, MESFUN16:51;
A72: dom (Integral2 (L-Meas,(R_EAL Pg21))) = REAL by FUNCT_2:def 1;
then A73: dom Pg1 = I ;
A74: Pg1 is continuous by A1, A2, A3, A70, Th18, MESFUN16:53;
then A75: ( Pg1 | I is bounded & Pg1 is_integrable_on I ) by A72, INTEGRA5:10, INTEGRA5:11;
(Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) . z1 = Integral ((Prod_Measure (L-Meas,L-Meas)),Pg21) by A69, A1, A2, A3, Th23
.= Integral ((Prod_Measure (L-Meas,L-Meas)),(R_EAL Pg21)) ;
then (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) . z1 = integral (Pg1,I) by A1, A2, A3, A70, Th18, MESFUN16:58;
then Gxy . zz1 = integral (Pg1,I) by A4, A69, FUNCT_1:49;
then A76: Gxy . zz1 = integral (Pg1,a,b) by A5, A8, XXREAL_1:29, INTEGRA5:def 4;
A77: dom (Pg1 - Pg0) = I /\ I by A32, A73, VALUED_1:12;
then A78: ( Pg1 - Pg0 is_integrable_on I & (Pg1 - Pg0) | I is bounded ) by A33, A74, INTEGRA5:10, INTEGRA5:11;
for x being Element of REAL st x in I holds
|.((Pg1 - Pg0) . x).| <= (r / 2) / (b - a)

proof

let x be Element of REAL ; :: thesis: ( x in I implies |.((Pg1 - Pg0) . x).| <= (r / 2) / (b - a) )
assume A79: x in I ; :: thesis: |.((Pg1 - Pg0) . x).| <= (r / 2) / (b - a)
reconsider Pg120 = ProjPMap1 (Pg20,x) as PartFunc of REAL,REAL ;
A80: dom Pg120 = J by A79, A29, MESFUN16:25;
ProjPMap1 ((R_EAL Pg20),x) = R_EAL (ProjPMap1 (Pg20,x)) by MESFUN16:31;
then A81: Pg120 = ProjPMap1 ((R_EAL Pg20),x) by MESFUNC5:def 7;
A82: Pg120 is continuous by A29, A30, MESFUN16:33;
A83: ( Pg120 | J is bounded & Pg120 is_integrable_on J ) by A29, A30, A79, A81, MESFUN16:40;
reconsider Pg121 = ProjPMap1 (Pg21,x) as PartFunc of REAL,REAL ;
A84: dom Pg121 = J by A79, A70, MESFUN16:25;
ProjPMap1 ((R_EAL Pg21),x) = R_EAL (ProjPMap1 (Pg21,x)) by MESFUN16:31;
then A85: Pg121 = ProjPMap1 ((R_EAL Pg21),x) by MESFUNC5:def 7;
A86: Pg121 is continuous by A70, A71, MESFUN16:33;
A87: ( Pg121 | J is bounded & Pg121 is_integrable_on J ) by A70, A71, A79, A85, MESFUN16:40;
Pg0 . x = (Integral2 (L-Meas,(R_EAL Pg20))) . x by A79, FUNCT_1:49;
then Pg0 . x = Integral (L-Meas,(ProjPMap1 ((R_EAL Pg20),x))) by MESFUN12:def 8;
then Pg0 . x = Integral (L-Meas,Pg120) by MESFUN16:31;
then A88: Pg0 . x = integral (Pg120,c,d) by A9, A12, A80, A83, XXREAL_1:29, MESFUN14:50;
Pg1 . x = (Integral2 (L-Meas,(R_EAL Pg21))) . x by A79, FUNCT_1:49;
then Pg1 . x = Integral (L-Meas,(ProjPMap1 ((R_EAL Pg21),x))) by MESFUN12:def 8;
then Pg1 . x = Integral (L-Meas,Pg121) by MESFUN16:31;
then Pg1 . x = integral (Pg121,c,d) by A9, A12, A84, A87, XXREAL_1:29, MESFUN14:50;
then A89: (Pg1 . x) - (Pg0 . x) = integral ((Pg121 - Pg120),c,d) by A9, A10, A12, A83, A87, A84, A80, A88, INTEGRA6:12;
A90: dom (Pg121 - Pg120) = J /\ J by A80, A84, VALUED_1:12;
then A91: ( (Pg121 - Pg120) | J is bounded & Pg121 - Pg120 is_integrable_on J ) by A82, A86, INTEGRA5:10, INTEGRA5:11;
for y being Real st y in J holds
|.((Pg121 - Pg120) . y).| <= (r / 2) / (b - a)

proof

let y be Real; :: thesis: ( y in J implies |.((Pg121 - Pg120) . y).| <= (r / 2) / (b - a) )
assume A92: y in J ; :: thesis: |.((Pg121 - Pg120) . y).| <= (r / 2) / (b - a)
reconsider yy = y as Element of REAL by XREAL_0:def 1;
A93: ( Pg120 . y = (ProjPMap1 ((ProjPMap2 ((R_EAL g),z0)),x)) . yy & Pg121 . y = (ProjPMap1 ((ProjPMap2 ((R_EAL g),z1)),x)) . yy ) by A81, A85, MESFUNC5:def 7;
A94: (Pg121 - Pg120) . y = (Pg121 . y) - (Pg120 . y) by A90, A92, VALUED_1:13
.= ((ProjPMap1 ((ProjPMap2 ((R_EAL g),z1)),x)) . yy) - ((ProjPMap1 ((ProjPMap2 ((R_EAL g),z0)),x)) . yy) by A93, Lm6 ;
|.(((ProjPMap1 ((ProjPMap2 ((R_EAL g),z1)),x)) . yy) - ((ProjPMap1 ((ProjPMap2 ((R_EAL g),z0)),x)) . yy)).| < (r / 2) / (b - a) by A28, A69, A79, A92, A68;
hence |.((Pg121 - Pg120) . y).| <= (r / 2) / (b - a) by A94, EXTREAL1:12; :: thesis: verum

end;

then |.(integral ((Pg121 - Pg120),c,d)).| <= ((r / 2) / (b - a)) * (d - c) by A9, A10, A11, A12, A90, A91, INTEGRA6:23;
hence |.((Pg1 - Pg0) . x).| <= (r / 2) / (b - a) by A64, A77, A79, A89, A67, VALUED_1:13; :: thesis: verum

end;

then for x being Real st x in ['a,b'] holds
|.((Pg1 - Pg0) . x).| <= (r / 2) / (b - a) by A5, A8;
then |.(integral ((Pg1 - Pg0),a,b)).| <= ((r / 2) / (b - a)) * (b - a) by A5, A6, A7, A8, A77, A78, INTEGRA6:23;
then |.(integral ((Pg1 - Pg0),a,b)).| <= r / 2 by A65, XCMPLX_1:87;
then |.(integral ((Pg1 - Pg0),a,b)).| < r by A66, XXREAL_0:2;
hence |.((Gxy . zz1) - (Gxy . zz0)).| < r by A5, A6, A8, A32, A34, A73, A75, A35, A76, INTEGRA6:12; :: thesis: verum

end;

hence ex s being Real st
( 0 < s & ( for z1 being Real st z1 in K & |.(z1 - zz0).| < s holds
|.((Gxy . z1) - (Gxy . zz0)).| < r ) ) by A68; :: thesis: verum

end;

suppose A95: ( a = b & c <> d ) ; :: thesis: ex s being Real st
( 0 < s & ( for z1 being Real st z1 in K & |.(z1 - zz0).| < s holds
|.((Gxy . z1) - (Gxy . zz0)).| < r ) )

then c < d by A10, XXREAL_0:1;
then A96: 0 < d - c by XREAL_1:50;
set r1 = r / 2;
( 0 < r / 2 & r / 2 < r ) by A28, XREAL_1:215, XREAL_1:216;
then consider s being Real such that
A97: ( 0 < s & ( for z1, z2 being Element of REAL st |.(z2 - z1).| < s & z1 in K & z2 in K holds
for x, y being Element of REAL st x in I & y in J holds
|.(((ProjPMap1 ((ProjPMap2 ((R_EAL g),z2)),x)) . y) - ((ProjPMap1 ((ProjPMap2 ((R_EAL g),z1)),x)) . y)).| < (r / 2) / (d - c) ) ) by A20, A96, XREAL_1:139;
for z1 being Real st z1 in K & |.(z1 - z0).| < s holds
|.((Gxy . z1) - (Gxy . zz0)).| < r

proof

let zz1 be Real; :: thesis: ( zz1 in K & |.(zz1 - z0).| < s implies |.((Gxy . zz1) - (Gxy . zz0)).| < r )
assume A98: ( zz1 in K & |.(zz1 - z0).| < s ) ; :: thesis: |.((Gxy . zz1) - (Gxy . zz0)).| < r
reconsider z1 = zz1 as Element of REAL by XREAL_0:def 1;
reconsider Pg21 = ProjPMap2 ((R_EAL g),z1) as PartFunc of [:REAL,REAL:],REAL by MESFUN16:30;
reconsider Pf21 = Pg21 as PartFunc of [:RNS_Real,RNS_Real:],RNS_Real ;
A99: dom Pg21 = [:I,J:] by A98, A1, A3, MESFUN16:28;
then A100: Pf21 is_continuous_on [:I,J:] by A1, A2, A3, Th18;
then reconsider Pg1 = (Integral2 (L-Meas,(R_EAL Pg21))) | I as PartFunc of REAL,REAL by A99, MESFUN16:51;
A101: dom (Integral2 (L-Meas,(R_EAL Pg21))) = REAL by FUNCT_2:def 1;
then A102: dom Pg1 = I ;
A103: Pg1 is continuous by A1, A2, A3, A99, Th18, MESFUN16:53;
then A104: ( Pg1 | I is bounded & Pg1 is_integrable_on I ) by A101, INTEGRA5:10, INTEGRA5:11;
(Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) . z1 = Integral ((Prod_Measure (L-Meas,L-Meas)),Pg21) by A98, A1, A2, A3, Th23
.= Integral ((Prod_Measure (L-Meas,L-Meas)),(R_EAL Pg21)) ;
then (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) . z1 = integral (Pg1,I) by A1, A2, A3, A99, Th18, MESFUN16:58;
then Gxy . zz1 = integral (Pg1,I) by A4, A98, FUNCT_1:49;
then A105: Gxy . zz1 = integral (Pg1,a,b) by A5, A8, XXREAL_1:29, INTEGRA5:def 4;
A106: dom (Pg1 - Pg0) = I /\ I by A32, A102, VALUED_1:12;
then A107: ( Pg1 - Pg0 is_integrable_on I & (Pg1 - Pg0) | I is bounded ) by A33, A103, INTEGRA5:10, INTEGRA5:11;
for x being Element of REAL st x in I holds
|.((Pg1 - Pg0) . x).| <= r / 2

proof

let x be Element of REAL ; :: thesis: ( x in I implies |.((Pg1 - Pg0) . x).| <= r / 2 )
assume A108: x in I ; :: thesis: |.((Pg1 - Pg0) . x).| <= r / 2
reconsider Pg120 = ProjPMap1 (Pg20,x) as PartFunc of REAL,REAL ;
A109: dom Pg120 = J by A108, A29, MESFUN16:25;
ProjPMap1 ((R_EAL Pg20),x) = R_EAL (ProjPMap1 (Pg20,x)) by MESFUN16:31;
then A110: Pg120 = ProjPMap1 ((R_EAL Pg20),x) by MESFUNC5:def 7;
A111: Pg120 is continuous by A29, A30, MESFUN16:33;
A112: ( Pg120 | J is bounded & Pg120 is_integrable_on J ) by A29, A30, A108, A110, MESFUN16:40;
reconsider Pg121 = ProjPMap1 (Pg21,x) as PartFunc of REAL,REAL ;
A113: dom Pg121 = J by A108, A99, MESFUN16:25;
ProjPMap1 ((R_EAL Pg21),x) = R_EAL (ProjPMap1 (Pg21,x)) by MESFUN16:31;
then A114: Pg121 = ProjPMap1 ((R_EAL Pg21),x) by MESFUNC5:def 7;
A115: Pg121 is continuous by A99, A100, MESFUN16:33;
A116: ( Pg121 | J is bounded & Pg121 is_integrable_on J ) by A99, A100, A108, A114, MESFUN16:40;
Pg0 . x = (Integral2 (L-Meas,(R_EAL Pg20))) . x by A108, FUNCT_1:49;
then Pg0 . x = Integral (L-Meas,(ProjPMap1 ((R_EAL Pg20),x))) by MESFUN12:def 8;
then Pg0 . x = Integral (L-Meas,Pg120) by MESFUN16:31;
then A117: Pg0 . x = integral (Pg120,c,d) by A9, A12, A109, A112, XXREAL_1:29, MESFUN14:50;
Pg1 . x = (Integral2 (L-Meas,(R_EAL Pg21))) . x by A108, FUNCT_1:49;
then Pg1 . x = Integral (L-Meas,(ProjPMap1 ((R_EAL Pg21),x))) by MESFUN12:def 8;
then Pg1 . x = Integral (L-Meas,Pg121) by MESFUN16:31;
then Pg1 . x = integral (Pg121,c,d) by A9, A12, A113, A116, XXREAL_1:29, MESFUN14:50;
then (Pg1 . x) - (Pg0 . x) = integral ((Pg121 - Pg120),c,d) by A9, A10, A12, A112, A116, A113, A109, A117, INTEGRA6:12;
then A118: (Pg1 - Pg0) . x = integral ((Pg121 - Pg120),c,d) by A106, A108, VALUED_1:13;
A119: dom (Pg121 - Pg120) = J /\ J by A109, A113, VALUED_1:12;
then A120: ( (Pg121 - Pg120) | J is bounded & Pg121 - Pg120 is_integrable_on J ) by A111, A115, INTEGRA5:10, INTEGRA5:11;
for y being Real st y in J holds
|.((Pg121 - Pg120) . y).| <= (r / 2) / (d - c)

proof

let y be Real; :: thesis: ( y in J implies |.((Pg121 - Pg120) . y).| <= (r / 2) / (d - c) )
assume A121: y in J ; :: thesis: |.((Pg121 - Pg120) . y).| <= (r / 2) / (d - c)
reconsider yy = y as Element of REAL by XREAL_0:def 1;
A122: ( Pg120 . y = (ProjPMap1 ((ProjPMap2 ((R_EAL g),z0)),x)) . yy & Pg121 . y = (ProjPMap1 ((ProjPMap2 ((R_EAL g),z1)),x)) . yy ) by A110, A114, MESFUNC5:def 7;
A123: (Pg121 - Pg120) . y = (Pg121 . y) - (Pg120 . y) by A119, A121, VALUED_1:13
.= ((ProjPMap1 ((ProjPMap2 ((R_EAL g),z1)),x)) . yy) - ((ProjPMap1 ((ProjPMap2 ((R_EAL g),z0)),x)) . yy) by A122, Lm6 ;
|.(((ProjPMap1 ((ProjPMap2 ((R_EAL g),z1)),x)) . yy) - ((ProjPMap1 ((ProjPMap2 ((R_EAL g),z0)),x)) . yy)).| < (r / 2) / (d - c) by A28, A98, A108, A121, A97;
hence |.((Pg121 - Pg120) . y).| <= (r / 2) / (d - c) by A123, EXTREAL1:12; :: thesis: verum

end;

then |.(integral ((Pg121 - Pg120),c,d)).| <= ((r / 2) / (d - c)) * (d - c) by A9, A10, A11, A12, A119, A120, INTEGRA6:23;
hence |.((Pg1 - Pg0) . x).| <= r / 2 by A118, A96, XCMPLX_1:87; :: thesis: verum

end;

then for x being Real st x in ['a,b'] holds
|.((Pg1 - Pg0) . x).| <= r / 2 by A5, A8;
then |.(integral ((Pg1 - Pg0),a,b)).| <= (r / 2) * (b - a) by A5, A6, A7, A8, A106, A107, INTEGRA6:23;
hence |.((Gxy . zz1) - (Gxy . zz0)).| < r by A5, A8, A32, A34, A95, A102, A104, A35, A105, A28, INTEGRA6:12; :: thesis: verum

end;

hence ex s being Real st
( 0 < s & ( for z1 being Real st z1 in K & |.(z1 - zz0).| < s holds
|.((Gxy . z1) - (Gxy . zz0)).| < r ) ) by A97; :: thesis: verum

end;

suppose ( a <> b & c <> d ) ; :: thesis: ex s being Real st
( 0 < s & ( for z1 being Real st z1 in K & |.(z1 - zz0).| < s holds
|.((Gxy . z1) - (Gxy . zz0)).| < r ) )

then ( a < b & c < d ) by A6, A10, XXREAL_0:1;
then A124: ( 0 < b - a & 0 < d - c ) by XREAL_1:50;
set r1 = r / 2;
A125: ( 0 < r / 2 & r / 2 < r ) by A28, XREAL_1:215, XREAL_1:216;
then 0 < (r / 2) / (b - a) by A124, XREAL_1:139;
then consider s being Real such that
A126: ( 0 < s & ( for z1, z2 being Element of REAL st |.(z2 - z1).| < s & z1 in K & z2 in K holds
for x, y being Element of REAL st x in I & y in J holds
|.(((ProjPMap1 ((ProjPMap2 ((R_EAL g),z2)),x)) . y) - ((ProjPMap1 ((ProjPMap2 ((R_EAL g),z1)),x)) . y)).| < ((r / 2) / (b - a)) / (d - c) ) ) by A20, A124, XREAL_1:139;
for z1 being Real st z1 in K & |.(z1 - z0).| < s holds
|.((Gxy . z1) - (Gxy . zz0)).| < r

proof

let zz1 be Real; :: thesis: ( zz1 in K & |.(zz1 - z0).| < s implies |.((Gxy . zz1) - (Gxy . zz0)).| < r )
assume A127: ( zz1 in K & |.(zz1 - z0).| < s ) ; :: thesis: |.((Gxy . zz1) - (Gxy . zz0)).| < r
reconsider z1 = zz1 as Element of REAL by XREAL_0:def 1;
reconsider Pg21 = ProjPMap2 ((R_EAL g),z1) as PartFunc of [:REAL,REAL:],REAL by MESFUN16:30;
reconsider Pf21 = Pg21 as PartFunc of [:RNS_Real,RNS_Real:],RNS_Real ;
A128: dom Pg21 = [:I,J:] by A127, A1, A3, MESFUN16:28;
then A129: Pf21 is_continuous_on [:I,J:] by A1, A2, A3, Th18;
then reconsider Pg1 = (Integral2 (L-Meas,(R_EAL Pg21))) | I as PartFunc of REAL,REAL by A128, MESFUN16:51;
A130: dom (Integral2 (L-Meas,(R_EAL Pg21))) = REAL by FUNCT_2:def 1;
then A131: dom Pg1 = I ;
A132: Pg1 is continuous by A1, A2, A3, A128, Th18, MESFUN16:53;
then A133: ( Pg1 | I is bounded & Pg1 is_integrable_on I ) by A130, INTEGRA5:10, INTEGRA5:11;
(Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) . z1 = Integral ((Prod_Measure (L-Meas,L-Meas)),Pg21) by A127, A1, A2, A3, Th23
.= Integral ((Prod_Measure (L-Meas,L-Meas)),(R_EAL Pg21)) ;
then (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) . z1 = integral (Pg1,I) by A1, A2, A3, A128, Th18, MESFUN16:58;
then Gxy . zz1 = integral (Pg1,I) by A4, A127, FUNCT_1:49;
then A134: Gxy . zz1 = integral (Pg1,a,b) by A5, A8, XXREAL_1:29, INTEGRA5:def 4;
A135: dom (Pg1 - Pg0) = I /\ I by A32, A131, VALUED_1:12;
then A136: ( Pg1 - Pg0 is_integrable_on I & (Pg1 - Pg0) | I is bounded ) by A33, A132, INTEGRA5:10, INTEGRA5:11;
for x being Element of REAL st x in I holds
|.((Pg1 - Pg0) . x).| <= (r / 2) / (b - a)

proof

let x be Element of REAL ; :: thesis: ( x in I implies |.((Pg1 - Pg0) . x).| <= (r / 2) / (b - a) )
assume A137: x in I ; :: thesis: |.((Pg1 - Pg0) . x).| <= (r / 2) / (b - a)
reconsider Pg120 = ProjPMap1 (Pg20,x) as PartFunc of REAL,REAL ;
A138: dom Pg120 = J by A137, A29, MESFUN16:25;
ProjPMap1 ((R_EAL Pg20),x) = R_EAL (ProjPMap1 (Pg20,x)) by MESFUN16:31;
then A139: Pg120 = ProjPMap1 ((R_EAL Pg20),x) by MESFUNC5:def 7;
A140: Pg120 is continuous by A29, A30, MESFUN16:33;
A141: ( Pg120 | J is bounded & Pg120 is_integrable_on J ) by A29, A30, A137, A139, MESFUN16:40;
reconsider Pg121 = ProjPMap1 (Pg21,x) as PartFunc of REAL,REAL ;
A142: dom Pg121 = J by A137, A128, MESFUN16:25;
ProjPMap1 ((R_EAL Pg21),x) = R_EAL (ProjPMap1 (Pg21,x)) by MESFUN16:31;
then A143: Pg121 = ProjPMap1 ((R_EAL Pg21),x) by MESFUNC5:def 7;
A144: Pg121 is continuous by A128, A129, MESFUN16:33;
A145: ( Pg121 | J is bounded & Pg121 is_integrable_on J ) by A128, A129, A137, A143, MESFUN16:40;
Pg0 . x = (Integral2 (L-Meas,(R_EAL Pg20))) . x by A137, FUNCT_1:49;
then Pg0 . x = Integral (L-Meas,(ProjPMap1 ((R_EAL Pg20),x))) by MESFUN12:def 8;
then Pg0 . x = Integral (L-Meas,Pg120) by MESFUN16:31;
then A146: Pg0 . x = integral (Pg120,c,d) by A9, A12, A138, A141, XXREAL_1:29, MESFUN14:50;
Pg1 . x = (Integral2 (L-Meas,(R_EAL Pg21))) . x by A137, FUNCT_1:49;
then Pg1 . x = Integral (L-Meas,(ProjPMap1 ((R_EAL Pg21),x))) by MESFUN12:def 8;
then Pg1 . x = Integral (L-Meas,Pg121) by MESFUN16:31;
then Pg1 . x = integral (Pg121,c,d) by A9, A12, A142, A145, XXREAL_1:29, MESFUN14:50;
then (Pg1 . x) - (Pg0 . x) = integral ((Pg121 - Pg120),c,d) by A9, A10, A12, A141, A145, A142, A138, A146, INTEGRA6:12;
then A147: (Pg1 - Pg0) . x = integral ((Pg121 - Pg120),c,d) by A135, A137, VALUED_1:13;
A148: dom (Pg121 - Pg120) = J /\ J by A138, A142, VALUED_1:12;
then A149: ( (Pg121 - Pg120) | J is bounded & Pg121 - Pg120 is_integrable_on J ) by A140, A144, INTEGRA5:10, INTEGRA5:11;
for y being Real st y in J holds
|.((Pg121 - Pg120) . y).| <= ((r / 2) / (b - a)) / (d - c)

proof

let y be Real; :: thesis: ( y in J implies |.((Pg121 - Pg120) . y).| <= ((r / 2) / (b - a)) / (d - c) )
assume A150: y in J ; :: thesis: |.((Pg121 - Pg120) . y).| <= ((r / 2) / (b - a)) / (d - c)
reconsider yy = y as Element of REAL by XREAL_0:def 1;
A151: ( Pg120 . y = (ProjPMap1 ((ProjPMap2 ((R_EAL g),z0)),x)) . yy & Pg121 . y = (ProjPMap1 ((ProjPMap2 ((R_EAL g),z1)),x)) . yy ) by A139, A143, MESFUNC5:def 7;
A152: (Pg121 - Pg120) . y = (Pg121 . y) - (Pg120 . y) by A148, A150, VALUED_1:13
.= ((ProjPMap1 ((ProjPMap2 ((R_EAL g),z1)),x)) . yy) - ((ProjPMap1 ((ProjPMap2 ((R_EAL g),z0)),x)) . yy) by A151, Lm6 ;
|.(((ProjPMap1 ((ProjPMap2 ((R_EAL g),z1)),x)) . yy) - ((ProjPMap1 ((ProjPMap2 ((R_EAL g),z0)),x)) . yy)).| < ((r / 2) / (b - a)) / (d - c) by A28, A127, A137, A150, A126;
hence |.((Pg121 - Pg120) . y).| <= ((r / 2) / (b - a)) / (d - c) by A152, EXTREAL1:12; :: thesis: verum

end;

then |.(integral ((Pg121 - Pg120),c,d)).| <= (((r / 2) / (b - a)) / (d - c)) * (d - c) by A9, A10, A11, A12, A148, A149, INTEGRA6:23;
hence |.((Pg1 - Pg0) . x).| <= (r / 2) / (b - a) by A147, A124, XCMPLX_1:87; :: thesis: verum

end;

then for x being Real st x in ['a,b'] holds
|.((Pg1 - Pg0) . x).| <= (r / 2) / (b - a) by A5, A8;
then |.(integral ((Pg1 - Pg0),a,b)).| <= ((r / 2) / (b - a)) * (b - a) by A5, A6, A7, A8, A135, A136, INTEGRA6:23;
then |.(integral ((Pg1 - Pg0),a,b)).| <= r / 2 by A124, XCMPLX_1:87;
then |.(integral ((Pg1 - Pg0),a,b)).| < r by A125, XXREAL_0:2;
hence |.((Gxy . zz1) - (Gxy . zz0)).| < r by A5, A6, A8, A32, A34, A131, A133, A35, A134, INTEGRA6:12; :: thesis: verum

end;

hence ex s being Real st
( 0 < s & ( for z1 being Real st z1 in K & |.(z1 - zz0).| < s holds
|.((Gxy . z1) - (Gxy . zz0)).| < r ) ) by A126; :: thesis: verum

end;

end;

end;

then Gxy | K is continuous by A4, A27, FCONT_1:14;
hence Gxy is continuous by A4; :: thesis: verum