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 st g = f * ((CarProd ((Seg n) --> REAL)) ") holds
( f is_integrable_on Prod_Measure (L-Meas n) iff g is_integrable_on XL-Meas n )
let f be PartFunc of (CarProduct ((Seg n) --> REAL)),ExtREAL; :: thesis: for g being PartFunc of (REAL n),ExtREAL st g = f * ((CarProd ((Seg n) --> REAL)) ") holds
( f is_integrable_on Prod_Measure (L-Meas n) iff g is_integrable_on XL-Meas n )
let g be PartFunc of (REAL n),ExtREAL; :: thesis: ( g = f * ((CarProd ((Seg n) --> REAL)) ") implies ( f is_integrable_on Prod_Measure (L-Meas n) iff g is_integrable_on XL-Meas n ) )
assume A1: g = f * ((CarProd ((Seg n) --> REAL)) ") ; :: thesis: ( f is_integrable_on Prod_Measure (L-Meas n) iff g is_integrable_on XL-Meas n )
product ((Seg n) --> REAL) = REAL n by SRINGS_5:8;
hence ( f is_integrable_on Prod_Measure (L-Meas n) iff g is_integrable_on XL-Meas n ) by A1, Th36; :: thesis: verum