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 st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
( ( for x being Element of REAL holds (Integral2 (L-Meas,|.(Integral2 (L-Meas,(R_EAL g))).|)) . x < +infty ) & ( for x being Element of REAL holds ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x) is_integrable_on L-Meas ) )
let f be PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
( ( for x being Element of REAL holds (Integral2 (L-Meas,|.(Integral2 (L-Meas,(R_EAL g))).|)) . x < +infty ) & ( for x being Element of REAL holds ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x) is_integrable_on L-Meas ) )
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis: ( [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g implies ( ( for x being Element of REAL holds (Integral2 (L-Meas,|.(Integral2 (L-Meas,(R_EAL g))).|)) . x < +infty ) & ( for x being Element of REAL holds ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x) is_integrable_on L-Meas ) ) )
assume that
A1: [:[:I,J:],K:] = dom f and
A2: f is_continuous_on [:[:I,J:],K:] and
A3: f = g ; :: thesis: ( ( for x being Element of REAL holds (Integral2 (L-Meas,|.(Integral2 (L-Meas,(R_EAL g))).|)) . x < +infty ) & ( for x being Element of REAL holds ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x) is_integrable_on L-Meas ) )
A4: dom (R_EAL g) = [:[:I,J:],K:] by A1, A3, MESFUNC5:def 7;
A5: [#] REAL = REAL by SUBSET_1:def 3;
A6: REAL in L-Field by PROB_1:5;
set Fz = Integral2 (L-Meas,(R_EAL g));
reconsider Gz = Integral2 (L-Meas,(R_EAL g)) as Function of [:REAL,REAL:],REAL by A1, A2, A3, Th32;
reconsider G = Gz | [:I,J:] as PartFunc of [:REAL,REAL:],REAL ;
reconsider F = G as PartFunc of [:RNS_Real,RNS_Real:],RNS_Real ;
A7: dom Gz = [:REAL,REAL:] by FUNCT_2:def 1;
F is_uniformly_continuous_on [:I,J:] by A1, A2, A3, Th34;
then A8: F is_continuous_on [:I,J:] by NFCONT_2:7;
thus A9: for x being Element of REAL holds (Integral2 (L-Meas,|.(Integral2 (L-Meas,(R_EAL g))).|)) . x < +infty :: thesis: for x being Element of REAL holds ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x) is_integrable_on L-Meas

proof

let x be Element of REAL ; :: thesis: (Integral2 (L-Meas,|.(Integral2 (L-Meas,(R_EAL g))).|)) . x < +infty
dom (Integral2 (L-Meas,(R_EAL g))) = [:REAL,REAL:] by FUNCT_2:def 1;
then dom |.(Integral2 (L-Meas,(R_EAL g))).| = [:REAL,REAL:] by MESFUNC1:def 10;
then A10: dom (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) = REAL by A5, MESFUN16:25;

per cases ( x in I or not x in I ) ;

suppose A11: x in I ; :: thesis: (Integral2 (L-Meas,|.(Integral2 (L-Meas,(R_EAL g))).|)) . x < +infty

A12: J misses REAL \ J by XBOOLE_1:79;
A13: J is Element of L-Field by MEASUR10:5, MEASUR12:75;
REAL in L-Field by PROB_1:5;
then reconsider NJ = REAL \ J as Element of L-Field by A13, PROB_1:6;
A14: J \/ NJ = REAL by XBOOLE_1:45;
set Fz1 = ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x);
set L0 = (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J;
set L1 = (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | NJ;

A15: now :: thesis: for y being Element of REAL st y in dom ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | NJ) holds
((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | NJ) . y = 0

let y be Element of REAL ; :: thesis: ( y in dom ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | NJ) implies ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | NJ) . y = 0 )
assume A16: y in dom ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | NJ) ; :: thesis: ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | NJ) . y = 0
then A17: ( y in REAL & not y in J ) by XBOOLE_0:def 5;
[x,y] in [:REAL,REAL:] ;
then [x,y] in dom (Integral2 (L-Meas,(R_EAL g))) by FUNCT_2:def 1;
then A18: [x,y] in dom |.(Integral2 (L-Meas,(R_EAL g))).| by MESFUNC1:def 10;
((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | NJ) . y = (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) . y by A16, FUNCT_1:49;
then ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | NJ) . y = |.(Integral2 (L-Meas,(R_EAL g))).| . (x,y) by A18, MESFUN12:def 3;
then A19: ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | NJ) . y = |.((Integral2 (L-Meas,(R_EAL g))) . (x,y)).| by A18, MESFUNC1:def 10;
A20: (Integral2 (L-Meas,(R_EAL g))) . (x,y) = Integral (L-Meas,(ProjPMap1 ((R_EAL g),[x,y]))) by MESFUN12:def 8;
not [x,y] in [:I,J:] by A17, ZFMISC_1:87;
then dom (ProjPMap1 ((R_EAL g),[x,y])) = {} by A4, MESFUN16:25;
hence ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | NJ) . y = 0 by A19, A20, EXTREAL1:16, MESFUN16:1; :: thesis: verum

end;

then A21: Integral (L-Meas,((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | NJ)) = 0 by A10, MESFUN12:57;
A22: for t being Element of REAL st t in J holds
0 <= ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J) . t

proof

let t be Element of REAL ; :: thesis: ( t in J implies 0 <= ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J) . t )
assume A23: t in J ; :: thesis: 0 <= ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J) . t
[x,t] in [:REAL,REAL:] ;
then [x,t] in dom (Integral2 (L-Meas,(R_EAL g))) by FUNCT_2:def 1;
then A24: [x,t] in dom |.(Integral2 (L-Meas,(R_EAL g))).| by MESFUNC1:def 10;
((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J) . t = (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) . t by FUNCT_1:49, A23;
then ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J) . t = |.(Integral2 (L-Meas,(R_EAL g))).| . (x,t) by A24, MESFUN12:def 3;
then ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J) . t = |.((Integral2 (L-Meas,(R_EAL g))) . (x,t)).| by A24, MESFUNC1:def 10;
hence 0 <= ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J) . t by EXTREAL1:14; :: thesis: verum

end;

Integral2 (L-Meas,(R_EAL g)) = R_EAL Gz by MESFUNC5:def 7;
then A25: |.(Integral2 (L-Meas,(R_EAL g))).| = R_EAL |.Gz.| by MESFUNC6:44;
then A26: |.(Integral2 (L-Meas,(R_EAL g))).| = |.Gz.| by MESFUNC5:def 7;
reconsider AFz = |.(Integral2 (L-Meas,(R_EAL g))).| as PartFunc of [:REAL,REAL:],REAL by A25, MESFUNC5:def 7;
R_EAL AFz = |.(Integral2 (L-Meas,(R_EAL g))).| by MESFUNC5:def 7;
then R_EAL (ProjPMap1 (AFz,x)) = ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x) by MESFUN16:31;
then ProjPMap1 (AFz,x) = ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x) by MESFUNC5:def 7;
then reconsider Gz1 = (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J as PartFunc of REAL,REAL by PARTFUN1:11;
A27: ProjPMap1 (|.G.|,x) is continuous by A7, A8, MESFUN16:34;
A28: J is Element of L-Field by MEASUR10:5, MEASUR12:75;
A29: dom Gz1 = J by A10;
J = X-section ([:I,J:],x) by A11, MEASUR11:22;
then A30: Gz1 = ProjPMap1 ((|.(Integral2 (L-Meas,(R_EAL g))).| | [:I,J:]),x) by MESFUN12:34;
|.(Integral2 (L-Meas,(R_EAL g))).| | [:I,J:] = |.G.| by A26, RFUNCT_1:46;
then |.(Integral2 (L-Meas,(R_EAL g))).| | [:I,J:] = R_EAL |.G.| by MESFUNC5:def 7;
then Gz1 = R_EAL (ProjPMap1 (|.G.|,x)) by A30, MESFUN16:31;
then Gz1 is continuous by A27, MESFUNC5:def 7;
then ( Gz1 || J is bounded & Gz1 is_integrable_on J ) by A10, INTEGRA5:10, INTEGRA5:11;
then Gz1 is_integrable_on L-Meas by A28, A29, MESFUN14:49;
then (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J is_integrable_on L-Meas by MESFUNC5:def 7;
then A31: Integral (L-Meas,((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J)) < +infty by MESFUNC5:96;
A32: for r being Element of REAL holds 0. <= (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) . r

proof

let r be Element of REAL ; :: thesis: 0. <= (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) . r

per cases ( r in J or r in NJ ) by A14, XBOOLE_0:def 3;

suppose A33: r in J ; :: thesis: 0. <= (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) . r

then 0 <= ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J) . r by A22;
hence 0 <= (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) . r by A33, FUNCT_1:49; :: thesis: verum

end;

suppose A34: r in NJ ; :: thesis: 0. <= (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) . r

then (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) . r = ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | NJ) . r by FUNCT_1:49;
hence 0 <= (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) . r by A15, A10, A34; :: thesis: verum

end;

end;

end;

reconsider H = REAL as Element of L-Field by PROB_1:5;
A35: ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x) is H -measurable by A1, A2, A3, A11, Th45;
A36: (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | (J \/ NJ) = ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x) by A14;
Integral (L-Meas,(ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x))) = (Integral (L-Meas,((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J))) + (Integral (L-Meas,((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | NJ))) by A10, A13, A32, A35, A12, A36, SUPINF_2:39, MESFUNC5:91;
then Integral (L-Meas,((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J)) = Integral (L-Meas,(ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x))) by A21, XXREAL_3:4;
hence (Integral2 (L-Meas,|.(Integral2 (L-Meas,(R_EAL g))).|)) . x < +infty by A31, MESFUN12:def 8; :: thesis: verum

end;

suppose A37: not x in I ; :: thesis: (Integral2 (L-Meas,|.(Integral2 (L-Meas,(R_EAL g))).|)) . x < +infty

now :: thesis: for y being Element of REAL st y in dom (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) holds
(ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) . y = 0

let y be Element of REAL ; :: thesis: ( y in dom (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) implies (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) . y = 0 )
assume y in dom (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) ; :: thesis: (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) . y = 0
[x,y] in [:REAL,REAL:] ;
then [x,y] in dom (Integral2 (L-Meas,(R_EAL g))) by FUNCT_2:def 1;
then A38: [x,y] in dom |.(Integral2 (L-Meas,(R_EAL g))).| by MESFUNC1:def 10;
then (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) . y = |.(Integral2 (L-Meas,(R_EAL g))).| . (x,y) by MESFUN12:def 3;
then A39: (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) . y = |.((Integral2 (L-Meas,(R_EAL g))) . (x,y)).| by A38, MESFUNC1:def 10;
A40: (Integral2 (L-Meas,(R_EAL g))) . (x,y) = Integral (L-Meas,(ProjPMap1 ((R_EAL g),[x,y]))) by MESFUN12:def 8;
not [x,y] in [:I,J:] by A37, ZFMISC_1:87;
then dom (ProjPMap1 ((R_EAL g),[x,y])) = {} by A4, MESFUN16:25;
hence (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) . y = 0 by A39, A40, EXTREAL1:16, MESFUN16:1; :: thesis: verum

end;

then Integral (L-Meas,(ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x))) = 0 by A10, A6, MESFUN12:57;
then (Integral2 (L-Meas,|.(Integral2 (L-Meas,(R_EAL g))).|)) . x = 0 by MESFUN12:def 8;
hence (Integral2 (L-Meas,|.(Integral2 (L-Meas,(R_EAL g))).|)) . x < +infty by XREAL_0:def 1, XXREAL_0:9; :: thesis: verum

end;

end;

end;

Integral2 (L-Meas,(R_EAL g)) is_integrable_on Prod_Measure (L-Meas,L-Meas) by A1, A2, A3, Th43;
hence for x being Element of REAL holds ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x) is_integrable_on L-Meas by A9, MESFUN13:32, MESFUN16:5; :: thesis: verum