theorem Th55: :: MESFUN17:55

for y 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,((ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | (REAL \ I))) = 0