let x be Element of REAL ; :: thesis: for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for P1Gz being PartFunc of REAL,REAL st x in I & [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & P1Gz = (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | J holds
( (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | J is_integrable_on L-Meas & integral (P1Gz,J) = Integral (L-Meas,((ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | J)) & integral (P1Gz,J) = Integral (L-Meas,(ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x))) & integral (P1Gz,J) = (Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g))))) . x )
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 P1Gz being PartFunc of REAL,REAL st x in I & [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & P1Gz = (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | J holds
( (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | J is_integrable_on L-Meas & integral (P1Gz,J) = Integral (L-Meas,((ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | J)) & integral (P1Gz,J) = Integral (L-Meas,(ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x))) & integral (P1Gz,J) = (Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g))))) . x )
let f be PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for P1Gz being PartFunc of REAL,REAL st x in I & [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & P1Gz = (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | J holds
( (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | J is_integrable_on L-Meas & integral (P1Gz,J) = Integral (L-Meas,((ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | J)) & integral (P1Gz,J) = Integral (L-Meas,(ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x))) & integral (P1Gz,J) = (Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g))))) . x )
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis: for P1Gz being PartFunc of REAL,REAL st x in I & [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & P1Gz = (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | J holds
( (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | J is_integrable_on L-Meas & integral (P1Gz,J) = Integral (L-Meas,((ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | J)) & integral (P1Gz,J) = Integral (L-Meas,(ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x))) & integral (P1Gz,J) = (Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g))))) . x )
let P1Gz be PartFunc of REAL,REAL; :: thesis: ( x in I & [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & P1Gz = (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | J implies ( (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | J is_integrable_on L-Meas & integral (P1Gz,J) = Integral (L-Meas,((ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | J)) & integral (P1Gz,J) = Integral (L-Meas,(ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x))) & integral (P1Gz,J) = (Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g))))) . x ) )
assume that
A1: x in I and
A2: [:[:I,J:],K:] = dom f and
A3: f is_continuous_on [:[:I,J:],K:] and
A4: f = g and
A5: P1Gz = (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | J ; :: thesis: ( (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | J is_integrable_on L-Meas & integral (P1Gz,J) = Integral (L-Meas,((ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | J)) & integral (P1Gz,J) = Integral (L-Meas,(ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x))) & integral (P1Gz,J) = (Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g))))) . x )
set Gz = Integral2 (L-Meas,(R_EAL g));
A6: J is Element of L-Field by MEASUR10:5, MEASUR12:75;
A7: ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x) is_integrable_on L-Meas by A2, A3, A4, Th46;
hence (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | J is_integrable_on L-Meas by A6, MESFUNC5:97; :: thesis: ( integral (P1Gz,J) = Integral (L-Meas,((ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | J)) & integral (P1Gz,J) = Integral (L-Meas,(ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x))) & integral (P1Gz,J) = (Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g))))) . x )
A8: dom (Integral2 (L-Meas,(R_EAL g))) = [:REAL,REAL:] by FUNCT_2:def 1;
[#] REAL = REAL by SUBSET_1:def 3;
then dom (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) = REAL by A8, MESFUN16:25;
then A9: dom P1Gz = J by A5;
( P1Gz || J is bounded & P1Gz is_integrable_on J ) by A1, A2, A3, A4, A5, Th59;
then ( P1Gz | J is_integrable_on L-Meas & Integral (L-Meas,(P1Gz | J)) = integral (P1Gz || J) ) by A6, A9, MESFUN14:49;
hence A10: integral (P1Gz,J) = Integral (L-Meas,((ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | J)) by A5, MESFUNC5:def 7; :: thesis: ( integral (P1Gz,J) = Integral (L-Meas,(ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x))) & integral (P1Gz,J) = (Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g))))) . x )
REAL in L-Field by PROB_1:5;
then reconsider NJ = REAL \ J as Element of L-Field by A6, PROB_1:6;
set PGz10 = (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | J;
set PGz11 = (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | NJ;
A11: Integral (L-Meas,((ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | NJ)) = 0 by A2, A4, Th54;
J \/ NJ = REAL by XBOOLE_1:45;
then (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | (J \/ NJ) = ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x) ;
then 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 A6, A7, XBOOLE_1:85, MESFUNC5:98;
hence integral (P1Gz,J) = Integral (L-Meas,(ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x))) by A10, A11, XXREAL_3:4; :: thesis: integral (P1Gz,J) = (Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g))))) . x
hence integral (P1Gz,J) = (Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g))))) . x by MESFUN12:def 8; :: thesis: verum