theorem :: MEASUR14:53

for f being PartFunc of [:[:REAL,REAL:],REAL:],ExtREAL
for g being PartFunc of (REAL 3),ExtREAL
for A being Element of sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field))
for B being Element of XL-Field 3 st g = f * ((CarProd ((Seg 3) --> REAL)) ") & B = (CarProd ((Seg 3) --> REAL)) .: A holds
( f is A -measurable iff g is B -measurable )