let n be non zero Nat; :: thesis: for f being PartFunc of (CarProduct ((Seg n) --> REAL)),ExtREAL
for g being PartFunc of (REAL n),ExtREAL
for A being Element of Prod_Field (L-Field n) st g = f * ((CarProd ((Seg n) --> REAL)) ") & A = dom f & f is A -measurable holds
Integral ((XL-Meas n),g) = Integral ((Prod_Measure (L-Meas n)),f)
let f be PartFunc of (CarProduct ((Seg n) --> REAL)),ExtREAL; :: thesis: for g being PartFunc of (REAL n),ExtREAL
for A being Element of Prod_Field (L-Field n) st g = f * ((CarProd ((Seg n) --> REAL)) ") & A = dom f & f is A -measurable holds
Integral ((XL-Meas n),g) = Integral ((Prod_Measure (L-Meas n)),f)
let g be PartFunc of (REAL n),ExtREAL; :: thesis: for A being Element of Prod_Field (L-Field n) st g = f * ((CarProd ((Seg n) --> REAL)) ") & A = dom f & f is A -measurable holds
Integral ((XL-Meas n),g) = Integral ((Prod_Measure (L-Meas n)),f)
let A be Element of Prod_Field (L-Field n); :: thesis: ( g = f * ((CarProd ((Seg n) --> REAL)) ") & A = dom f & f is A -measurable implies Integral ((XL-Meas n),g) = Integral ((Prod_Measure (L-Meas n)),f) )
assume that
A1: g = f * ((CarProd ((Seg n) --> REAL)) ") and
A2: A = dom f and
A3: f is A -measurable ; :: thesis: Integral ((XL-Meas n),g) = Integral ((Prod_Measure (L-Meas n)),f)
product ((Seg n) --> REAL) = REAL n by SRINGS_5:8;
hence Integral ((XL-Meas n),g) = Integral ((Prod_Measure (L-Meas n)),f) by A1, A2, A3, Th12, Th32; :: thesis: verum