theorem Th54: :: MESFUN17:54

for x being Element of REAL
for I, J, K being non empty closed_interval Subset of REAL
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom g holds
Integral (L-Meas,((ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | (REAL \ J))) = 0