theorem :: MEASUR14:51

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