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 x being Element of REAL
for E being Element of L-Field st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & x in I holds
ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x) is E -measurable
let f be PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for x being Element of REAL
for E being Element of L-Field st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & x in I holds
ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x) is E -measurable
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis: for x being Element of REAL
for E being Element of L-Field st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & x in I holds
ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x) is E -measurable
let x be Element of REAL ; :: thesis: for E being Element of L-Field st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & x in I holds
ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x) is E -measurable
let E be Element of L-Field ; :: thesis: ( [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & x in I implies ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x) is E -measurable )
assume that
A1: [:[:I,J:],K:] = dom f and
A2: f is_continuous_on [:[:I,J:],K:] and
A3: f = g and
A4: x in I ; :: thesis: ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x) is E -measurable
A5: dom (R_EAL g) = [:[:I,J:],K:] by A1, A3, MESFUNC5:def 7;
A6: [#] REAL = REAL by SUBSET_1:def 3;
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;
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 A9: dom (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) = REAL by A6, MESFUN16:25;
A10: 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 A10, PROB_1:6;
A11: J \/ NJ = REAL by XBOOLE_1:45;
A12: J /\ NJ = {} by XBOOLE_1:85, XBOOLE_0:def 7;
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;
A13: dom ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J) = J by A9;

A14: 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 A15: 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 A16: ( 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 A17: [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 A15, FUNCT_1:49;
then ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | NJ) . y = |.(Integral2 (L-Meas,(R_EAL g))).| . (x,y) by A17, MESFUN12:def 3;
then A18: ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | NJ) . y = |.((Integral2 (L-Meas,(R_EAL g))) . (x,y)).| by A17, MESFUNC1:def 10;
A19: (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 A16, ZFMISC_1:87;
then dom (ProjPMap1 ((R_EAL g),[x,y])) = {} by A5, MESFUN16:25;
hence ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | NJ) . y = 0 by A18, A19, EXTREAL1:16, MESFUN16:1; :: thesis: verum

end;

A20: 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 A21: 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 A22: [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, A21;
then ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J) . t = |.(Integral2 (L-Meas,(R_EAL g))).| . (x,t) by A22, MESFUN12:def 3;
then ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J) . t = |.((Integral2 (L-Meas,(R_EAL g))) . (x,t)).| by A22, 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 A23: |.(Integral2 (L-Meas,(R_EAL g))).| = R_EAL |.Gz.| by MESFUNC6:44;
then A24: |.(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 A23, 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;
A25: ProjPMap1 (|.G.|,x) is continuous by A7, A8, MESFUN16:34;
A26: J is Element of L-Field by MEASUR10:5, MEASUR12:75;
A27: dom Gz1 = J by A9;
J = X-section ([:I,J:],x) by A4, MEASUR11:22;
then A28: Gz1 = ProjPMap1 ((|.(Integral2 (L-Meas,(R_EAL g))).| | [:I,J:]),x) by MESFUN12:34;
|.(Integral2 (L-Meas,(R_EAL g))).| | [:I,J:] = |.G.| by A24, 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 A28, MESFUN16:31;
then Gz1 is continuous by A25, MESFUNC5:def 7;
then ( Gz1 || J is bounded & Gz1 is_integrable_on J ) by A9, INTEGRA5:10, INTEGRA5:11;
then Gz1 is_integrable_on L-Meas by A26, A27, MESFUN14:49;
then A29: (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J is_integrable_on L-Meas by MESFUNC5:def 7;
reconsider H = REAL as Element of L-Field by PROB_1:5;
for r being Real holds H /\ (less_dom ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)),r)) in L-Field

proof

let r be Real; :: thesis: H /\ (less_dom ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)),r)) in L-Field
consider H0 being Element of L-Field such that
A30: ( H0 = dom ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J) & (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J is H0 -measurable ) by A29, MESFUNC5:def 17;

per cases ( r <= 0 or 0 < r ) ;

suppose A31: r <= 0 ; :: thesis: H /\ (less_dom ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)),r)) in L-Field

less_dom ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)),r) = {}

proof

assume less_dom ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)),r) <> {} ; :: thesis: contradiction
then consider x being object such that
A32: x in less_dom ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)),r) by XBOOLE_0:def 1;
A33: (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) . x < r by MESFUNC1:def 11, A32;

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

suppose A34: x in J ; :: thesis: contradiction

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

end;

suppose not x in J ; :: thesis: contradiction

then A35: x in NJ by A32, XBOOLE_0:def 5;
then (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) . x = ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | NJ) . x by FUNCT_1:49;
hence contradiction by A14, A9, A35, A31, A33; :: thesis: verum

end;

end;

end;

hence H /\ (less_dom ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)),r)) in L-Field by PROB_1:4; :: thesis: verum

end;

suppose A36: 0 < r ; :: thesis: H /\ (less_dom ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)),r)) in L-Field

A37: for z being object holds
( z in less_dom ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)),r) iff z in (less_dom (((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J),r)) \/ NJ )

proof

let z be object ; :: thesis: ( z in less_dom ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)),r) iff z in (less_dom (((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J),r)) \/ NJ )

hereby :: thesis: ( z in (less_dom (((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J),r)) \/ NJ implies z in less_dom ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)),r) )

assume A38: z in less_dom ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)),r) ; :: thesis: z in (less_dom (((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J),r)) \/ NJ
then A39: ( z in dom (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) & (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) . z < r ) by MESFUNC1:def 11;

per cases ( z in J or z in NJ ) by A38, A11, XBOOLE_0:def 3;

suppose A40: z in J ; :: thesis: z in (less_dom (((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J),r)) \/ NJ

then ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J) . z < r by FUNCT_1:49, A39;
then z in less_dom (((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J),r) by A13, A40, MESFUNC1:def 11;
hence z in (less_dom (((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J),r)) \/ NJ by XBOOLE_0:def 3; :: thesis: verum

end;

suppose z in NJ ; :: thesis: z in (less_dom (((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J),r)) \/ NJ

hence z in (less_dom (((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J),r)) \/ NJ by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

assume z in (less_dom (((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J),r)) \/ NJ ; :: thesis: z in less_dom ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)),r)

per cases then ( z in less_dom (((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J),r) or z in NJ ) by XBOOLE_0:def 3;

suppose A41: z in less_dom (((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J),r) ; :: thesis: z in less_dom ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)),r)

then ( z in dom ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J) & ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J) . z < r ) by MESFUNC1:def 11;
then (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) . z < r by FUNCT_1:49;
hence z in less_dom ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)),r) by A9, A41, MESFUNC1:def 11; :: thesis: verum

end;

suppose A42: z in NJ ; :: thesis: z in less_dom ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)),r)

then reconsider u = z as Element of REAL ;
(ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) . u = ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | NJ) . z by A42, FUNCT_1:49;
then (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) . u = 0 by A14, A42, A9;
hence z in less_dom ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)),r) by A9, A36, MESFUNC1:def 11; :: thesis: verum

end;

end;

end;

A43: H /\ (less_dom ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)),r)) = (J \/ NJ) /\ (less_dom ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)),r)) by XBOOLE_1:45
.= (J \/ NJ) /\ ((less_dom (((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J),r)) \/ NJ) by A37, TARSKI:2
.= (J /\ ((less_dom (((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J),r)) \/ NJ)) \/ (NJ /\ ((less_dom (((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J),r)) \/ NJ)) by XBOOLE_1:23 ;
J /\ ((less_dom (((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J),r)) \/ NJ) = (J /\ (less_dom (((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J),r))) \/ {} by A12, XBOOLE_1:23;
then A44: J /\ ((less_dom (((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J),r)) \/ NJ) in L-Field by A9, A30;
A45: less_dom (((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J),r) c= J by A13, MESFUNC1:def 11;
NJ /\ ((less_dom (((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J),r)) \/ NJ) = (NJ /\ (less_dom (((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J),r))) \/ (NJ /\ NJ) by XBOOLE_1:23;
then NJ /\ ((less_dom (((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) | J),r)) \/ NJ) = {} \/ (NJ /\ NJ) by A45;
hence H /\ (less_dom ((ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)),r)) in L-Field by A43, A44, PROB_1:3; :: thesis: verum

end;

end;

end;

then ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x) is H -measurable ;
hence ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x) is E -measurable by MESFUNC1:30; :: thesis: verum