let n be non zero Nat; :: thesis: for X being non-empty n -element FinSequence
for S being sigmaFieldFamily of X
for m being sigmaMeasureFamily of S
for f being PartFunc of (CarProduct X),ExtREAL
for g being PartFunc of (product X),ExtREAL
for A being Element of Prod_Field S
for B being Element of XProd_Field S st B = (CarProd X) .: A & g = f * ((CarProd X) ") holds
( f is A -measurable iff g is B -measurable )
let X be non-empty n -element FinSequence; :: thesis: for S being sigmaFieldFamily of X
for m being sigmaMeasureFamily of S
for f being PartFunc of (CarProduct X),ExtREAL
for g being PartFunc of (product X),ExtREAL
for A being Element of Prod_Field S
for B being Element of XProd_Field S st B = (CarProd X) .: A & g = f * ((CarProd X) ") holds
( f is A -measurable iff g is B -measurable )
let S be sigmaFieldFamily of X; :: thesis: for m being sigmaMeasureFamily of S
for f being PartFunc of (CarProduct X),ExtREAL
for g being PartFunc of (product X),ExtREAL
for A being Element of Prod_Field S
for B being Element of XProd_Field S st B = (CarProd X) .: A & g = f * ((CarProd X) ") holds
( f is A -measurable iff g is B -measurable )
let m be sigmaMeasureFamily of S; :: thesis: for f being PartFunc of (CarProduct X),ExtREAL
for g being PartFunc of (product X),ExtREAL
for A being Element of Prod_Field S
for B being Element of XProd_Field S st B = (CarProd X) .: A & g = f * ((CarProd X) ") holds
( f is A -measurable iff g is B -measurable )
let f be PartFunc of (CarProduct X),ExtREAL; :: thesis: for g being PartFunc of (product X),ExtREAL
for A being Element of Prod_Field S
for B being Element of XProd_Field S st B = (CarProd X) .: A & g = f * ((CarProd X) ") holds
( f is A -measurable iff g is B -measurable )
let g be PartFunc of (product X),ExtREAL; :: thesis: for A being Element of Prod_Field S
for B being Element of XProd_Field S st B = (CarProd X) .: A & g = f * ((CarProd X) ") holds
( f is A -measurable iff g is B -measurable )
let A be Element of Prod_Field S; :: thesis: for B being Element of XProd_Field S st B = (CarProd X) .: A & g = f * ((CarProd X) ") holds
( f is A -measurable iff g is B -measurable )
let B be Element of XProd_Field S; :: thesis: ( B = (CarProd X) .: A & g = f * ((CarProd X) ") implies ( f is A -measurable iff g is B -measurable ) )
assume A1: ( B = (CarProd X) .: A & g = f * ((CarProd X) ") ) ; :: thesis: ( f is A -measurable iff g is B -measurable )
CarProd X is bijective by Th12;
hence ( f is A -measurable iff g is B -measurable ) by Th20, A1; :: thesis: verum