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 z being Element of REAL holds ProjPMap2 ((R_EAL g),z) is_integrable_on Prod_Measure (L-Meas,L-Meas) ) & ( for V being Element of L-Field holds Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) is V -measurable ) & Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) is_integrable_on L-Meas & Integral ((Prod_Measure ((Prod_Measure (L-Meas,L-Meas)),L-Meas)),g) = Integral (L-Meas,(Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)))) )
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 z being Element of REAL holds ProjPMap2 ((R_EAL g),z) is_integrable_on Prod_Measure (L-Meas,L-Meas) ) & ( for V being Element of L-Field holds Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) is V -measurable ) & Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) is_integrable_on L-Meas & Integral ((Prod_Measure ((Prod_Measure (L-Meas,L-Meas)),L-Meas)),g) = Integral (L-Meas,(Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)))) )
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 z being Element of REAL holds ProjPMap2 ((R_EAL g),z) is_integrable_on Prod_Measure (L-Meas,L-Meas) ) & ( for V being Element of L-Field holds Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) is V -measurable ) & Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) is_integrable_on L-Meas & Integral ((Prod_Measure ((Prod_Measure (L-Meas,L-Meas)),L-Meas)),g) = Integral (L-Meas,(Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)))) ) )
assume that
A1: [:[:I,J:],K:] = dom f and
A2: f is_continuous_on [:[:I,J:],K:] and
A3: f = g ; :: thesis: ( ( for z being Element of REAL holds ProjPMap2 ((R_EAL g),z) is_integrable_on Prod_Measure (L-Meas,L-Meas) ) & ( for V being Element of L-Field holds Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) is V -measurable ) & Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) is_integrable_on L-Meas & Integral ((Prod_Measure ((Prod_Measure (L-Meas,L-Meas)),L-Meas)),g) = Integral (L-Meas,(Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)))) )
A4: g is_integrable_on Prod_Measure ((Prod_Measure (L-Meas,L-Meas)),L-Meas) by A1, A2, A3, Th43;
for z being Element of REAL holds (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z < +infty by A1, A2, A3, Th41;
hence ( ( for z being Element of REAL holds ProjPMap2 ((R_EAL g),z) is_integrable_on Prod_Measure (L-Meas,L-Meas) ) & ( for V being Element of L-Field holds Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) is V -measurable ) & Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) is_integrable_on L-Meas & Integral ((Prod_Measure ((Prod_Measure (L-Meas,L-Meas)),L-Meas)),g) = Integral (L-Meas,(Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)))) ) by A4, MESFUN13:33, MESFUN16:5, MESFUN16:6; :: thesis: verum