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 st g = f * ((CarProd X) ") holds
( f is_integrable_on Prod_Measure m iff g is_integrable_on XProd_Measure m )
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 st g = f * ((CarProd X) ") holds
( f is_integrable_on Prod_Measure m iff g is_integrable_on XProd_Measure m )
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 st g = f * ((CarProd X) ") holds
( f is_integrable_on Prod_Measure m iff g is_integrable_on XProd_Measure m )
let m be sigmaMeasureFamily of S; :: thesis: for f being PartFunc of (CarProduct X),ExtREAL
for g being PartFunc of (product X),ExtREAL st g = f * ((CarProd X) ") holds
( f is_integrable_on Prod_Measure m iff g is_integrable_on XProd_Measure m )
let f be PartFunc of (CarProduct X),ExtREAL; :: thesis: for g being PartFunc of (product X),ExtREAL st g = f * ((CarProd X) ") holds
( f is_integrable_on Prod_Measure m iff g is_integrable_on XProd_Measure m )
let g be PartFunc of (product X),ExtREAL; :: thesis: ( g = f * ((CarProd X) ") implies ( f is_integrable_on Prod_Measure m iff g is_integrable_on XProd_Measure m ) )
assume A1: g = f * ((CarProd X) ") ; :: thesis: ( f is_integrable_on Prod_Measure m iff g is_integrable_on XProd_Measure m )
CarProd X is bijective by Th12;
hence ( f is_integrable_on Prod_Measure m iff g is_integrable_on XProd_Measure m ) by Th33, A1; :: thesis: verum