let f be PartFunc of [:REAL,REAL:],ExtREAL; :: thesis: 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 )
let g be PartFunc of (REAL 2),ExtREAL; :: thesis: 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 )
let A be Element of sigma (measurable_rectangles (L-Field,L-Field)); :: thesis: 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 )
let B be Element of XL-Field 2; :: thesis: ( g = f * ((CarProd ((Seg 2) --> REAL)) ") & B = (CarProd ((Seg 2) --> REAL)) .: A implies ( f is A -measurable iff g is B -measurable ) )
assume that
A1: g = f * ((CarProd ((Seg 2) --> REAL)) ") and
A2: B = (CarProd ((Seg 2) --> REAL)) .: A ; :: thesis: ( f is A -measurable iff g is B -measurable )
Prod_Field (L-Field (1 + 1)) = sigma (measurable_rectangles ((Prod_Field (L-Field 1)),L-Field)) by Th44;
then reconsider A1 = A as Element of Prod_Field (L-Field 2) by Th37, Th41;
reconsider f1 = f as PartFunc of (CarProduct ((Seg 2) --> REAL)),ExtREAL by Th37;
( f1 is A1 -measurable iff g is B -measurable ) by A1, A2, Th49;
hence ( f is A -measurable iff g is B -measurable ) by Th50; :: thesis: verum