theorem Th54: :: MESFUN16:54

for I, J being non empty closed_interval Subset of REAL
for g being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for f being PartFunc of [:REAL,REAL:],REAL st [:I,J:] = dom g & g is_continuous_on [:I,J:] & g = f holds
( (Integral1 (L-Meas,|.(R_EAL f).|)) | J is PartFunc of REAL,REAL & (Integral1 (L-Meas,(R_EAL f))) | J is PartFunc of REAL,REAL )