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, Th10;
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;
dom |.(R_EAL g).| = dom (R_EAL g) by MESFUNC1:def 10;
then 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 A20: [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] )
[x,y,z] in dom g by A19, A20, A1, A3, ZFMISC_1:87;
then A21: [x,y,z] in dom |.g.| by VALUED_1:def 11;
A22: (R_EAL g) . ([x,y],z) = g . [x,y,z] by MESFUNC5:def 7;
|.(R_EAL g).| . ([x,y],z) = |.((R_EAL g) . [x,y,z]).| by A19, A20, A17, ZFMISC_1:87, MESFUNC1:def 10;
hence |.(R_EAL g).| . ([x,y],z) = |.(g . [x,y,z]).| by A22, EXTREAL1:12; :: thesis: |.(R_EAL g).| . ([x,y],z) = |.g.| . [x,y,z]
hence |.(R_EAL g).| . ([x,y],z) = |.g.| . [x,y,z] by VALUED_1:def 11, A21; :: thesis: verum

end;

A23: 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
A24: ( 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 A24; :: 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 A25: ( |.(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 A26: ( 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 A27: |.((|.g.| . [x,y,z2]) - (|.g.| . [x,y,z1])).| < e by A24, A25;
a27: (|.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 A25, A1, A3, MESFUN16:28;
then A28: (ProjPMap1 ((ProjPMap2 (|.(R_EAL g).|,z1)),x)) . y = (ProjPMap2 (|.(R_EAL g).|,z1)) . (x,y) by A26, ZFMISC_1:87, MESFUN12:def 3;
dom (ProjPMap2 (|.(R_EAL g).|,z2)) = [:I,J:] by A25, A1, A3, MESFUN16:28;
then A29: (ProjPMap1 ((ProjPMap2 (|.(R_EAL g).|,z2)),x)) . y = (ProjPMap2 (|.(R_EAL g).|,z2)) . (x,y) by A26, 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, A25, A26;
hence |.(((ProjPMap1 ((ProjPMap2 (|.(R_EAL g).|,z2)),x)) . y) - ((ProjPMap1 ((ProjPMap2 (|.(R_EAL g).|,z1)),x)) . y)).| < e by A27, a27, A28, A29, EXTREAL1:12; :: thesis: verum

end;

A30: 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 A31: ( 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 ;
A32: dom Pg20 = [:I,J:] by A31, A1, A3, MESFUN16:28;
then A33: Pf20 is_continuous_on [:I,J:] by A1, A2, A3, Th20;
then reconsider Pg0 = (Integral2 (L-Meas,(R_EAL Pg20))) | I as PartFunc of REAL,REAL by A32, MESFUN16:51;
A34: dom (Integral2 (L-Meas,(R_EAL Pg20))) = REAL by FUNCT_2:def 1;
then A35: dom Pg0 = I ;
A36: Pg0 is continuous by A1, A2, A3, A32, Th20, MESFUN16:53;
then A37: ( Pg0 | I is bounded & Pg0 is_integrable_on I ) by A34, INTEGRA5:10, INTEGRA5:11;
(Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z0 = Integral ((Prod_Measure (L-Meas,L-Meas)),Pg20) by A31, A1, A2, A3, Th28
.= 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, A32, Th20, MESFUN16:58;
then Gxy . zz0 = integral (Pg0,I) by A4, A31, FUNCT_1:49;
then A38: 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 A39: ( 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
A40: ( 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 A23, A31;
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 A41: ( 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 ;
A42: dom Pg21 = [:I,J:] by A41, A1, A3, MESFUN16:28;
then A43: Pf21 is_continuous_on [:I,J:] by A1, A2, A3, Th20;
then reconsider Pg1 = (Integral2 (L-Meas,(R_EAL Pg21))) | I as PartFunc of REAL,REAL by A42, MESFUN16:51;
A44: dom (Integral2 (L-Meas,(R_EAL Pg21))) = REAL by FUNCT_2:def 1;
then A45: dom Pg1 = I ;
A46: Pg1 is continuous by A1, A2, A3, A42, Th20, MESFUN16:53;
then A47: ( Pg1 | I is bounded & Pg1 is_integrable_on I ) by A44, INTEGRA5:10, INTEGRA5:11;
(Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z1 = Integral ((Prod_Measure (L-Meas,L-Meas)),Pg21) by A41, A1, A2, A3, Th28
.= 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, A42, Th20, MESFUN16:58;
then Gxy . zz1 = integral (Pg1,I) by A4, A41, FUNCT_1:49;
then A48: Gxy . zz1 = integral (Pg1,a,b) by A5, A8, XXREAL_1:29, INTEGRA5:def 4;
A49: dom (Pg1 - Pg0) = I /\ I by A35, A45, VALUED_1:12;
then A50: ( Pg1 - Pg0 is_integrable_on I & (Pg1 - Pg0) | I is bounded ) by A36, A46, 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 A51: x in I ; :: thesis: |.((Pg1 - Pg0) . x).| <= r
reconsider Pg120 = ProjPMap1 (Pg20,x) as PartFunc of REAL,REAL ;
A52: dom Pg120 = J by A51, A32, MESFUN16:25;
ProjPMap1 ((R_EAL Pg20),x) = R_EAL (ProjPMap1 (Pg20,x)) by MESFUN16:31;
then A53: Pg120 = ProjPMap1 ((R_EAL Pg20),x) by MESFUNC5:def 7;
A54: Pg120 is continuous by A32, A33, MESFUN16:33;
A55: ( Pg120 | J is bounded & Pg120 is_integrable_on J ) by A32, A33, A51, A53, MESFUN16:40;
reconsider Pg121 = ProjPMap1 (Pg21,x) as PartFunc of REAL,REAL ;
A56: dom Pg121 = J by A51, A42, MESFUN16:25;
ProjPMap1 ((R_EAL Pg21),x) = R_EAL (ProjPMap1 (Pg21,x)) by MESFUN16:31;
then A57: Pg121 = ProjPMap1 ((R_EAL Pg21),x) by MESFUNC5:def 7;
A58: Pg121 is continuous by A42, A43, MESFUN16:33;
A59: ( Pg121 | J is bounded & Pg121 is_integrable_on J ) by A42, A43, A51, A57, MESFUN16:40;
Pg0 . x = (Integral2 (L-Meas,(R_EAL Pg20))) . x by A51, 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 A60: Pg0 . x = integral (Pg120,c,d) by A9, A12, A52, A55, XXREAL_1:29, MESFUN14:50;
Pg1 . x = (Integral2 (L-Meas,(R_EAL Pg21))) . x by A51, 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, A56, A59, XXREAL_1:29, MESFUN14:50;
then A61: (Pg1 . x) - (Pg0 . x) = integral ((Pg121 - Pg120),c,d) by A9, A10, A12, A55, A59, A56, A52, A60, INTEGRA6:12;
A62: dom (Pg121 - Pg120) = J /\ J by A52, A56, VALUED_1:12;
then A63: ( (Pg121 - Pg120) | J is bounded & Pg121 - Pg120 is_integrable_on J ) by A54, A58, 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 A64: y in J ; :: thesis: |.((Pg121 - Pg120) . y).| <= r
reconsider yy = y as Element of REAL by XREAL_0:def 1;
A65: Pg120 . y = (ProjPMap1 ((ProjPMap2 (|.(R_EAL g).|,z0)),x)) . yy by A53, MESFUNC5:def 7;
A66: Pg121 . y = (ProjPMap1 ((ProjPMap2 (|.(R_EAL g).|,z1)),x)) . yy by A57, MESFUNC5:def 7;
A67: (Pg121 - Pg120) . y = (Pg121 . y) - (Pg120 . y) by A62, A64, VALUED_1:13
.= ((ProjPMap1 ((ProjPMap2 (|.(R_EAL g).|,z1)),x)) . yy) - ((ProjPMap1 ((ProjPMap2 (|.(R_EAL g).|,z0)),x)) . yy) by A66, A65, Lm6 ;
|.(((ProjPMap1 ((ProjPMap2 (|.(R_EAL g).|,z1)),x)) . yy) - ((ProjPMap1 ((ProjPMap2 (|.(R_EAL g).|,z0)),x)) . yy)).| < r by A31, A41, A51, A64, A40;
hence |.((Pg121 - Pg120) . y).| <= r by A67, EXTREAL1:12; :: thesis: verum

end;

then |.(integral ((Pg121 - Pg120),c,d)).| <= r * (d - c) by A9, A10, A11, A12, A62, A63, INTEGRA6:23;
hence |.((Pg1 - Pg0) . x).| <= r by A31, A39, A49, A51, A61, 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, A49, A50, INTEGRA6:23;
hence |.((Gxy . zz1) - (Gxy . zz0)).| < r by A5, A8, A31, A39, A35, A37, A45, A47, A38, A48, 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 A40; :: thesis: verum

end;

suppose A68: ( 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 A69: 0 < b - a by XREAL_1:50;
set r1 = r / 2;
A70: ( 0 < r / 2 & r / 2 < r ) by A31, XREAL_1:215, XREAL_1:216;
then A71: 0 < (r / 2) / (b - a) by A69, XREAL_1:139;
consider s being Real such that
A72: ( 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 A23, A69, A70, 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 A73: ( 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 ;
A74: dom Pg21 = [:I,J:] by A73, A1, A3, MESFUN16:28;
then A75: Pf21 is_continuous_on [:I,J:] by A1, A2, A3, Th20;
then reconsider Pg1 = (Integral2 (L-Meas,(R_EAL Pg21))) | I as PartFunc of REAL,REAL by A74, MESFUN16:51;
A76: dom (Integral2 (L-Meas,(R_EAL Pg21))) = REAL by FUNCT_2:def 1;
then A77: dom Pg1 = I ;
A78: Pg1 is continuous by A1, A2, A3, A74, Th20, MESFUN16:53;
then A79: ( Pg1 | I is bounded & Pg1 is_integrable_on I ) by A76, INTEGRA5:10, INTEGRA5:11;
(Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z1 = Integral ((Prod_Measure (L-Meas,L-Meas)),Pg21) by A73, A1, A2, A3, Th28
.= 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, A74, Th20, MESFUN16:58;
then Gxy . zz1 = integral (Pg1,I) by A4, A73, FUNCT_1:49;
then A80: Gxy . zz1 = integral (Pg1,a,b) by A5, A8, XXREAL_1:29, INTEGRA5:def 4;
A81: dom (Pg1 - Pg0) = I /\ I by A35, A77, VALUED_1:12;
then A82: ( Pg1 - Pg0 is_integrable_on I & (Pg1 - Pg0) | I is bounded ) by A36, A78, 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 A83: x in I ; :: thesis: |.((Pg1 - Pg0) . x).| <= (r / 2) / (b - a)
reconsider Pg120 = ProjPMap1 (Pg20,x) as PartFunc of REAL,REAL ;
A84: dom Pg120 = J by A83, A32, MESFUN16:25;
ProjPMap1 ((R_EAL Pg20),x) = R_EAL (ProjPMap1 (Pg20,x)) by MESFUN16:31;
then A85: Pg120 = ProjPMap1 ((R_EAL Pg20),x) by MESFUNC5:def 7;
A86: Pg120 is continuous by A32, A33, MESFUN16:33;
A87: ( Pg120 | J is bounded & Pg120 is_integrable_on J ) by A32, A33, A83, A85, MESFUN16:40;
reconsider Pg121 = ProjPMap1 (Pg21,x) as PartFunc of REAL,REAL ;
A88: dom Pg121 = J by A83, A74, MESFUN16:25;
ProjPMap1 ((R_EAL Pg21),x) = R_EAL (ProjPMap1 (Pg21,x)) by MESFUN16:31;
then A89: Pg121 = ProjPMap1 ((R_EAL Pg21),x) by MESFUNC5:def 7;
A90: Pg121 is continuous by A74, A75, MESFUN16:33;
A91: ( Pg121 | J is bounded & Pg121 is_integrable_on J ) by A74, A75, A83, A89, MESFUN16:40;
Pg0 . x = (Integral2 (L-Meas,(R_EAL Pg20))) . x by A83, 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 A92: Pg0 . x = integral (Pg120,c,d) by A9, A12, A84, A87, XXREAL_1:29, MESFUN14:50;
Pg1 . x = (Integral2 (L-Meas,(R_EAL Pg21))) . x by A83, 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, A88, A91, XXREAL_1:29, MESFUN14:50;
then A93: (Pg1 . x) - (Pg0 . x) = integral ((Pg121 - Pg120),c,d) by A9, A10, A12, A87, A91, A88, A84, A92, INTEGRA6:12;
A94: dom (Pg121 - Pg120) = J /\ J by A84, A88, VALUED_1:12;
then A95: ( (Pg121 - Pg120) | J is bounded & Pg121 - Pg120 is_integrable_on J ) by A86, A90, 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 A96: y in J ; :: thesis: |.((Pg121 - Pg120) . y).| <= (r / 2) / (b - a)
reconsider yy = y as Element of REAL by XREAL_0:def 1;
A97: ( Pg120 . y = (ProjPMap1 ((ProjPMap2 (|.(R_EAL g).|,z0)),x)) . yy & Pg121 . y = (ProjPMap1 ((ProjPMap2 (|.(R_EAL g).|,z1)),x)) . yy ) by A85, A89, MESFUNC5:def 7;
A98: (Pg121 - Pg120) . y = (Pg121 . y) - (Pg120 . y) by A94, A96, VALUED_1:13
.= ((ProjPMap1 ((ProjPMap2 (|.(R_EAL g).|,z1)),x)) . yy) - ((ProjPMap1 ((ProjPMap2 (|.(R_EAL g).|,z0)),x)) . yy) by A97, Lm6 ;
|.(((ProjPMap1 ((ProjPMap2 (|.(R_EAL g).|,z1)),x)) . yy) - ((ProjPMap1 ((ProjPMap2 (|.(R_EAL g).|,z0)),x)) . yy)).| < (r / 2) / (b - a) by A31, A73, A83, A96, A72;
hence |.((Pg121 - Pg120) . y).| <= (r / 2) / (b - a) by A98, EXTREAL1:12; :: thesis: verum

end;

then |.(integral ((Pg121 - Pg120),c,d)).| <= ((r / 2) / (b - a)) * (d - c) by A9, A10, A11, A12, A94, A95, INTEGRA6:23;
hence |.((Pg1 - Pg0) . x).| <= (r / 2) / (b - a) by A68, A93, A71, A81, A83, 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, A81, A82, INTEGRA6:23;
then |.(integral ((Pg1 - Pg0),a,b)).| <= r / 2 by A69, XCMPLX_1:87;
then |.(integral ((Pg1 - Pg0),a,b)).| < r by A70, XXREAL_0:2;
hence |.((Gxy . zz1) - (Gxy . zz0)).| < r by A5, A6, A8, A35, A37, A77, A79, A38, A80, 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 A72; :: thesis: verum

end;

suppose A99: ( 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 A100: 0 < d - c by XREAL_1:50;
set r1 = r / 2;
( 0 < r / 2 & r / 2 < r ) by A31, XREAL_1:215, XREAL_1:216;
then consider s being Real such that
A101: ( 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 A23, A100, 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 A102: ( 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 ;
A103: dom Pg21 = [:I,J:] by A102, A1, A3, MESFUN16:28;
then A104: Pf21 is_continuous_on [:I,J:] by A1, A2, A3, Th20;
then reconsider Pg1 = (Integral2 (L-Meas,(R_EAL Pg21))) | I as PartFunc of REAL,REAL by A103, MESFUN16:51;
A105: dom (Integral2 (L-Meas,(R_EAL Pg21))) = REAL by FUNCT_2:def 1;
then A106: dom Pg1 = I ;
A107: Pg1 is continuous by A1, A2, A3, A103, Th20, MESFUN16:53;
then A108: ( Pg1 | I is bounded & Pg1 is_integrable_on I ) by A105, INTEGRA5:10, INTEGRA5:11;
(Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z1 = Integral ((Prod_Measure (L-Meas,L-Meas)),Pg21) by A102, A1, A2, A3, Th28
.= 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, A103, Th20, MESFUN16:58;
then Gxy . zz1 = integral (Pg1,I) by A4, A102, FUNCT_1:49;
then A109: Gxy . zz1 = integral (Pg1,a,b) by A5, A8, XXREAL_1:29, INTEGRA5:def 4;
A110: dom (Pg1 - Pg0) = I /\ I by A35, A106, VALUED_1:12;
then A111: ( Pg1 - Pg0 is_integrable_on I & (Pg1 - Pg0) | I is bounded ) by A36, A107, 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 A112: x in I ; :: thesis: |.((Pg1 - Pg0) . x).| <= r / 2
reconsider Pg120 = ProjPMap1 (Pg20,x) as PartFunc of REAL,REAL ;
A113: dom Pg120 = J by A112, A32, MESFUN16:25;
ProjPMap1 ((R_EAL Pg20),x) = R_EAL (ProjPMap1 (Pg20,x)) by MESFUN16:31;
then A114: Pg120 = ProjPMap1 ((R_EAL Pg20),x) by MESFUNC5:def 7;
A115: Pg120 is continuous by A32, A33, MESFUN16:33;
A116: ( Pg120 | J is bounded & Pg120 is_integrable_on J ) by A32, A33, A112, A114, MESFUN16:40;
reconsider Pg121 = ProjPMap1 (Pg21,x) as PartFunc of REAL,REAL ;
A117: dom Pg121 = J by A112, A103, MESFUN16:25;
ProjPMap1 ((R_EAL Pg21),x) = R_EAL (ProjPMap1 (Pg21,x)) by MESFUN16:31;
then A118: Pg121 = ProjPMap1 ((R_EAL Pg21),x) by MESFUNC5:def 7;
A119: Pg121 is continuous by A103, A104, MESFUN16:33;
A120: ( Pg121 | J is bounded & Pg121 is_integrable_on J ) by A103, A104, A112, A118, MESFUN16:40;
Pg0 . x = (Integral2 (L-Meas,(R_EAL Pg20))) . x by A112, 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 A121: Pg0 . x = integral (Pg120,c,d) by A9, A12, A113, A116, XXREAL_1:29, MESFUN14:50;
Pg1 . x = (Integral2 (L-Meas,(R_EAL Pg21))) . x by A112, 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, A117, A120, XXREAL_1:29, MESFUN14:50;
then (Pg1 . x) - (Pg0 . x) = integral ((Pg121 - Pg120),c,d) by A9, A10, A12, A116, A120, A117, A113, A121, INTEGRA6:12;
then A122: (Pg1 - Pg0) . x = integral ((Pg121 - Pg120),c,d) by A110, A112, VALUED_1:13;
A123: dom (Pg121 - Pg120) = J /\ J by A113, A117, VALUED_1:12;
then A124: ( (Pg121 - Pg120) | J is bounded & Pg121 - Pg120 is_integrable_on J ) by A115, A119, 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 A125: y in J ; :: thesis: |.((Pg121 - Pg120) . y).| <= (r / 2) / (d - c)
reconsider yy = y as Element of REAL by XREAL_0:def 1;
A126: ( Pg120 . y = (ProjPMap1 ((ProjPMap2 (|.(R_EAL g).|,z0)),x)) . yy & Pg121 . y = (ProjPMap1 ((ProjPMap2 (|.(R_EAL g).|,z1)),x)) . yy ) by A114, A118, MESFUNC5:def 7;
A127: (Pg121 - Pg120) . y = (Pg121 . y) - (Pg120 . y) by A123, A125, VALUED_1:13
.= ((ProjPMap1 ((ProjPMap2 (|.(R_EAL g).|,z1)),x)) . yy) - ((ProjPMap1 ((ProjPMap2 (|.(R_EAL g).|,z0)),x)) . yy) by A126, Lm6 ;
|.(((ProjPMap1 ((ProjPMap2 (|.(R_EAL g).|,z1)),x)) . yy) - ((ProjPMap1 ((ProjPMap2 (|.(R_EAL g).|,z0)),x)) . yy)).| < (r / 2) / (d - c) by A31, A102, A112, A125, A101;
hence |.((Pg121 - Pg120) . y).| <= (r / 2) / (d - c) by A127, EXTREAL1:12; :: thesis: verum

end;

then |.(integral ((Pg121 - Pg120),c,d)).| <= ((r / 2) / (d - c)) * (d - c) by A9, A10, A11, A12, A123, A124, INTEGRA6:23;
hence |.((Pg1 - Pg0) . x).| <= r / 2 by A122, A100, 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, A110, A111, INTEGRA6:23;
hence |.((Gxy . zz1) - (Gxy . zz0)).| < r by A5, A8, A99, A35, A37, A106, A108, A38, A109, A31, 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 A101; :: 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 A128: ( 0 < b - a & 0 < d - c ) by XREAL_1:50;
set r1 = r / 2;
A129: ( 0 < r / 2 & r / 2 < r ) by A31, XREAL_1:215, XREAL_1:216;
then 0 < (r / 2) / (b - a) by A128, XREAL_1:139;
then consider s being Real such that
A130: ( 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 A23, A128, 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 A131: ( 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 ;
A132: dom Pg21 = [:I,J:] by A131, A1, A3, MESFUN16:28;
then A133: Pf21 is_continuous_on [:I,J:] by A1, A2, A3, Th20;
then reconsider Pg1 = (Integral2 (L-Meas,(R_EAL Pg21))) | I as PartFunc of REAL,REAL by A132, MESFUN16:51;
A134: dom (Integral2 (L-Meas,(R_EAL Pg21))) = REAL by FUNCT_2:def 1;
then A135: dom Pg1 = I ;
A136: Pg1 is continuous by A1, A2, A3, A132, Th20, MESFUN16:53;
then A137: ( Pg1 | I is bounded & Pg1 is_integrable_on I ) by A134, INTEGRA5:10, INTEGRA5:11;
(Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z1 = Integral ((Prod_Measure (L-Meas,L-Meas)),Pg21) by A131, A1, A2, A3, Th28
.= 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, A132, Th20, MESFUN16:58;
then Gxy . zz1 = integral (Pg1,I) by A4, A131, FUNCT_1:49;
then A138: Gxy . zz1 = integral (Pg1,a,b) by A5, A8, XXREAL_1:29, INTEGRA5:def 4;
A139: dom (Pg1 - Pg0) = I /\ I by A35, A135, VALUED_1:12;
then A140: ( Pg1 - Pg0 is_integrable_on I & (Pg1 - Pg0) | I is bounded ) by A36, A136, 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 A141: x in I ; :: thesis: |.((Pg1 - Pg0) . x).| <= (r / 2) / (b - a)
reconsider Pg120 = ProjPMap1 (Pg20,x) as PartFunc of REAL,REAL ;
A142: dom Pg120 = J by A141, A32, MESFUN16:25;
ProjPMap1 ((R_EAL Pg20),x) = R_EAL (ProjPMap1 (Pg20,x)) by MESFUN16:31;
then A143: Pg120 = ProjPMap1 ((R_EAL Pg20),x) by MESFUNC5:def 7;
A144: Pg120 is continuous by A32, A33, MESFUN16:33;
A145: ( Pg120 | J is bounded & Pg120 is_integrable_on J ) by A32, A33, A141, A143, MESFUN16:40;
reconsider Pg121 = ProjPMap1 (Pg21,x) as PartFunc of REAL,REAL ;
A146: dom Pg121 = J by A141, A132, MESFUN16:25;
ProjPMap1 ((R_EAL Pg21),x) = R_EAL (ProjPMap1 (Pg21,x)) by MESFUN16:31;
then A147: Pg121 = ProjPMap1 ((R_EAL Pg21),x) by MESFUNC5:def 7;
A148: Pg121 is continuous by A132, A133, MESFUN16:33;
A149: ( Pg121 | J is bounded & Pg121 is_integrable_on J ) by A132, A133, A141, A147, MESFUN16:40;
Pg0 . x = (Integral2 (L-Meas,(R_EAL Pg20))) . x by A141, 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 A150: Pg0 . x = integral (Pg120,c,d) by A9, A12, A142, A145, XXREAL_1:29, MESFUN14:50;
Pg1 . x = (Integral2 (L-Meas,(R_EAL Pg21))) . x by A141, 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, A146, A149, XXREAL_1:29, MESFUN14:50;
then (Pg1 . x) - (Pg0 . x) = integral ((Pg121 - Pg120),c,d) by A9, A10, A12, A145, A149, A146, A142, A150, INTEGRA6:12;
then A151: (Pg1 - Pg0) . x = integral ((Pg121 - Pg120),c,d) by A139, A141, VALUED_1:13;
A152: dom (Pg121 - Pg120) = J /\ J by A142, A146, VALUED_1:12;
then A153: ( (Pg121 - Pg120) | J is bounded & Pg121 - Pg120 is_integrable_on J ) by A144, A148, 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 A154: 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;
A155: ( Pg120 . y = (ProjPMap1 ((ProjPMap2 (|.(R_EAL g).|,z0)),x)) . yy & Pg121 . y = (ProjPMap1 ((ProjPMap2 (|.(R_EAL g).|,z1)),x)) . yy ) by A143, A147, MESFUNC5:def 7;
A156: (Pg121 - Pg120) . y = (Pg121 . y) - (Pg120 . y) by A152, A154, VALUED_1:13
.= ((ProjPMap1 ((ProjPMap2 (|.(R_EAL g).|,z1)),x)) . yy) - ((ProjPMap1 ((ProjPMap2 (|.(R_EAL g).|,z0)),x)) . yy) by A155, Lm6 ;
|.(((ProjPMap1 ((ProjPMap2 (|.(R_EAL g).|,z1)),x)) . yy) - ((ProjPMap1 ((ProjPMap2 (|.(R_EAL g).|,z0)),x)) . yy)).| < ((r / 2) / (b - a)) / (d - c) by A31, A131, A141, A154, A130;
hence |.((Pg121 - Pg120) . y).| <= ((r / 2) / (b - a)) / (d - c) by A156, EXTREAL1:12; :: thesis: verum

end;

then |.(integral ((Pg121 - Pg120),c,d)).| <= (((r / 2) / (b - a)) / (d - c)) * (d - c) by A9, A10, A11, A12, A152, A153, INTEGRA6:23;
hence |.((Pg1 - Pg0) . x).| <= (r / 2) / (b - a) by A151, A128, 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, A139, A140, INTEGRA6:23;
then |.(integral ((Pg1 - Pg0),a,b)).| <= r / 2 by A128, XCMPLX_1:87;
then |.(integral ((Pg1 - Pg0),a,b)).| < r by A129, XXREAL_0:2;
hence |.((Gxy . zz1) - (Gxy . zz0)).| < r by A5, A6, A8, A35, A37, A135, A137, A38, A138, 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 A130; :: thesis: verum

end;

end;

end;

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