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