let y 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 P2Gz being PartFunc of REAL,REAL st y in J & [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & P2Gz = (ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | I holds
( (ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | I is_integrable_on L-Meas & integral (P2Gz,I) = Integral (L-Meas,((ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | I)) & integral (P2Gz,I) = Integral (L-Meas,(ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y))) & integral (P2Gz,I) = (Integral1 (L-Meas,(Integral2 (L-Meas,(R_EAL g))))) . y )
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 P2Gz being PartFunc of REAL,REAL st y in J & [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & P2Gz = (ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | I holds
( (ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | I is_integrable_on L-Meas & integral (P2Gz,I) = Integral (L-Meas,((ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | I)) & integral (P2Gz,I) = Integral (L-Meas,(ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y))) & integral (P2Gz,I) = (Integral1 (L-Meas,(Integral2 (L-Meas,(R_EAL g))))) . y )
let f be PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for P2Gz being PartFunc of REAL,REAL st y in J & [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & P2Gz = (ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | I holds
( (ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | I is_integrable_on L-Meas & integral (P2Gz,I) = Integral (L-Meas,((ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | I)) & integral (P2Gz,I) = Integral (L-Meas,(ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y))) & integral (P2Gz,I) = (Integral1 (L-Meas,(Integral2 (L-Meas,(R_EAL g))))) . y )
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis: for P2Gz being PartFunc of REAL,REAL st y in J & [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & P2Gz = (ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | I holds
( (ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | I is_integrable_on L-Meas & integral (P2Gz,I) = Integral (L-Meas,((ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | I)) & integral (P2Gz,I) = Integral (L-Meas,(ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y))) & integral (P2Gz,I) = (Integral1 (L-Meas,(Integral2 (L-Meas,(R_EAL g))))) . y )
let P2Gz be PartFunc of REAL,REAL; :: thesis: ( y in J & [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & P2Gz = (ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | I implies ( (ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | I is_integrable_on L-Meas & integral (P2Gz,I) = Integral (L-Meas,((ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | I)) & integral (P2Gz,I) = Integral (L-Meas,(ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y))) & integral (P2Gz,I) = (Integral1 (L-Meas,(Integral2 (L-Meas,(R_EAL g))))) . y ) )
assume that
A1: y in J and
A2: [:[:I,J:],K:] = dom f and
A3: f is_continuous_on [:[:I,J:],K:] and
A4: f = g and
A5: P2Gz = (ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | I ; :: thesis: ( (ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | I is_integrable_on L-Meas & integral (P2Gz,I) = Integral (L-Meas,((ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | I)) & integral (P2Gz,I) = Integral (L-Meas,(ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y))) & integral (P2Gz,I) = (Integral1 (L-Meas,(Integral2 (L-Meas,(R_EAL g))))) . y )
set Gz = Integral2 (L-Meas,(R_EAL g));
A6: I is Element of L-Field by MEASUR10:5, MEASUR12:75;
A7: ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y) is_integrable_on L-Meas by A2, A3, A4, Th48;
hence (ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | I is_integrable_on L-Meas by A6, MESFUNC5:97; :: thesis: ( integral (P2Gz,I) = Integral (L-Meas,((ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | I)) & integral (P2Gz,I) = Integral (L-Meas,(ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y))) & integral (P2Gz,I) = (Integral1 (L-Meas,(Integral2 (L-Meas,(R_EAL g))))) . y )
A8: dom (Integral2 (L-Meas,(R_EAL g))) = [:REAL,REAL:] by FUNCT_2:def 1;
[#] REAL = REAL by SUBSET_1:def 3;
then dom (ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) = REAL by A8, MESFUN16:26;
then A9: dom P2Gz = I by A5;
( P2Gz || I is bounded & P2Gz is_integrable_on I ) by A1, A2, A3, A4, A5, Th60;
then ( P2Gz | I is_integrable_on L-Meas & Integral (L-Meas,(P2Gz | I)) = integral (P2Gz || I) ) by A6, A9, MESFUN14:49;
hence A10: integral (P2Gz,I) = Integral (L-Meas,((ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | I)) by A5, MESFUNC5:def 7; :: thesis: ( integral (P2Gz,I) = Integral (L-Meas,(ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y))) & integral (P2Gz,I) = (Integral1 (L-Meas,(Integral2 (L-Meas,(R_EAL g))))) . y )
REAL in L-Field by PROB_1:5;
then reconsider NI = REAL \ I as Element of L-Field by A6, PROB_1:6;
set PGz20 = (ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | I;
set PGz21 = (ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | NI;
A11: Integral (L-Meas,((ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | NI)) = 0 by A2, A4, Th55;
I \/ NI = REAL by XBOOLE_1:45;
then (ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | (I \/ NI) = ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y) ;
then Integral (L-Meas,(ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y))) = (Integral (L-Meas,((ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | I))) + (Integral (L-Meas,((ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | NI))) by A6, A7, XBOOLE_1:85, MESFUNC5:98;
hence integral (P2Gz,I) = Integral (L-Meas,(ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y))) by A10, A11, XXREAL_3:4; :: thesis: integral (P2Gz,I) = (Integral1 (L-Meas,(Integral2 (L-Meas,(R_EAL g))))) . y
hence integral (P2Gz,I) = (Integral1 (L-Meas,(Integral2 (L-Meas,(R_EAL g))))) . y by MESFUN12:def 7; :: thesis: verum