let f1 be PartFunc of [:[:REAL,REAL:],REAL:],ExtREAL; :: thesis: for f2 being PartFunc of (CarProduct ((Seg 3) --> REAL)),ExtREAL
for A1 being Element of sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field))
for A2 being Element of Prod_Field (L-Field 3) st f1 = f2 & A1 = A2 holds
( f1 is A1 -measurable iff f2 is A2 -measurable )
let f2 be PartFunc of (CarProduct ((Seg 3) --> REAL)),ExtREAL; :: thesis: for A1 being Element of sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field))
for A2 being Element of Prod_Field (L-Field 3) st f1 = f2 & A1 = A2 holds
( f1 is A1 -measurable iff f2 is A2 -measurable )
let A1 be Element of sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field)); :: thesis: for A2 being Element of Prod_Field (L-Field 3) st f1 = f2 & A1 = A2 holds
( f1 is A1 -measurable iff f2 is A2 -measurable )
let A2 be Element of Prod_Field (L-Field 3); :: thesis: ( f1 = f2 & A1 = A2 implies ( f1 is A1 -measurable iff f2 is A2 -measurable ) )
assume that
A1: f1 = f2 and
A2: A1 = A2 ; :: thesis: ( f1 is A1 -measurable iff f2 is A2 -measurable )
( Prod_Field (L-Field (2 + 1)) = sigma (measurable_rectangles ((Prod_Field (L-Field 2)),L-Field)) & Prod_Field (L-Field (1 + 1)) = sigma (measurable_rectangles ((Prod_Field (L-Field 1)),L-Field)) ) by Th44;
hence ( f1 is A1 -measurable iff f2 is A2 -measurable ) by A1, A2, Th37, Th41; :: thesis: verum