let x be Element of REAL ; :: thesis:
let I, J, K be non empty closed_interval Subset of REAL; :: thesis:
let f be PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real; :: thesis:
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis:
let P1Gz be PartFunc of REAL,REAL; :: thesis:
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))) | [:I,J:]),x) ; :: thesis:
reconsider Gz = (Integral2 (L-Meas,(R_EAL g))) | [:I,J:] as PartFunc of [:REAL,REAL:],REAL by A2, A3, A4, Th32;
reconsider Fz = Gz as PartFunc of [:RNS_Real,RNS_Real:],RNS_Real ;
A6: dom (Integral2 (L-Meas,(R_EAL g))) = [:REAL,REAL:] by FUNCT_2:def 1;
A7: P1Gz = ProjPMap1 ((R_EAL Gz),x) by A5, MESFUNC5:def 7;
A8: Fz is_uniformly_continuous_on [:I,J:] by A2, A3, A4, Th34;
hence P1Gz is continuous by A6, A7, NFCONT_2:7, MESFUN16:36; :: thesis:
dom (ProjPMap1 ((R_EAL Gz),x)) = J by A6, A1, A8, MESFUN16:27;
hence dom (ProjPMap1 (((Integral2 (L-Meas,(R_EAL g))) | [:I,J:]),x)) = J by MESFUNC5:def 7; :: thesis:
A9: Fz is_continuous_on [:I,J:] by A8, NFCONT_2:7;
hence ( P1Gz | J is bounded & P1Gz is_integrable_on J ) by A6, A7, A1, MESFUN16:40; :: thesis:
A10: ( P1Gz is_integrable_on L-Meas & integral (P1Gz,J) = Integral (L-Meas,(ProjPMap1 ((R_EAL Gz),x))) & (Integral2 (L-Meas,(R_EAL Gz))) . x = integral (P1Gz,J) ) by A6, A7, A9, A1, MESFUN16:41;
hence ( integral (P1Gz,J) = Integral (L-Meas,(ProjPMap1 (((Integral2 (L-Meas,(R_EAL g))) | [:I,J:]),x))) & integral (P1Gz,J) = (Integral2 (L-Meas,((Integral2 (L-Meas,(R_EAL g))) | [:I,J:]))) . x ) by MESFUNC5:def 7; :: thesis:
ProjPMap1 ((R_EAL Gz),x) is_integrable_on L-Meas by A10, A7, MESFUNC5:def 7;
hence ProjPMap1 (((Integral2 (L-Meas,(R_EAL g))) | [:I,J:]),x) is_integrable_on L-Meas by MESFUNC5:def 7; :: thesis: