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)
for B being Element of XL-Field n st g = f * ((CarProd ((Seg n) --> REAL)) ") & B = (CarProd ((Seg n) --> REAL)) .: A holds
( f is A -measurable iff g is B -measurable )
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)
for B being Element of XL-Field n st g = f * ((CarProd ((Seg n) --> REAL)) ") & B = (CarProd ((Seg n) --> REAL)) .: A holds
( f is A -measurable iff g is B -measurable )
let g be PartFunc of (REAL n),ExtREAL; :: thesis: for A being Element of Prod_Field (L-Field n)
for B being Element of XL-Field n st g = f * ((CarProd ((Seg n) --> REAL)) ") & B = (CarProd ((Seg n) --> REAL)) .: A holds
( f is A -measurable iff g is B -measurable )
let A be Element of Prod_Field (L-Field n); :: thesis: for B being Element of XL-Field n st g = f * ((CarProd ((Seg n) --> REAL)) ") & B = (CarProd ((Seg n) --> REAL)) .: A holds
( f is A -measurable iff g is B -measurable )
let B be Element of XL-Field n; :: thesis: ( g = f * ((CarProd ((Seg n) --> REAL)) ") & B = (CarProd ((Seg n) --> REAL)) .: A implies ( f is A -measurable iff g is B -measurable ) )
assume that
A1: g = f * ((CarProd ((Seg n) --> REAL)) ") and
A2: B = (CarProd ((Seg n) --> REAL)) .: A ; :: thesis: ( f is A -measurable iff g is B -measurable )
product ((Seg n) --> REAL) = REAL n by SRINGS_5:8;
hence ( f is A -measurable iff g is B -measurable ) by A1, A2, Th34; :: thesis: verum