theorem Th27: :: MESFUN17:27

for I, J being non empty closed_interval Subset of REAL
for K being Subset of REAL
for z being Element of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for Pg2 being PartFunc of [:REAL,REAL:],REAL
for E being Element of sigma (measurable_rectangles (L-Field,L-Field)) st z in K & dom f = [:[:I,J:],K:] & f is_continuous_on [:[:I,J:],K:] & f = g & Pg2 = ProjPMap2 (|.(R_EAL g).|,z) & E = [:I,J:] holds
Pg2 is E -measurable