let n be non zero Nat; :: thesis: for D being n -element FinSequence
for I being Subset of (CarProduct ((Seg n) --> RNS_Real))
for J being Interval st ( for i being Nat st i in Seg n holds
D . i is Interval ) & I = CarProduct D holds
( [:I,J:] is Subset of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:] & [:I,J:] in sigma (measurable_rectangles ((Prod_Field (L-Field n)),L-Field)) )
let D be n -element FinSequence; :: thesis: for I being Subset of (CarProduct ((Seg n) --> RNS_Real))
for J being Interval st ( for i being Nat st i in Seg n holds
D . i is Interval ) & I = CarProduct D holds
( [:I,J:] is Subset of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:] & [:I,J:] in sigma (measurable_rectangles ((Prod_Field (L-Field n)),L-Field)) )
let I be Subset of (CarProduct ((Seg n) --> RNS_Real)); :: thesis: for J being Interval st ( for i being Nat st i in Seg n holds
D . i is Interval ) & I = CarProduct D holds
( [:I,J:] is Subset of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:] & [:I,J:] in sigma (measurable_rectangles ((Prod_Field (L-Field n)),L-Field)) )
let J be Interval; :: thesis: ( ( for i being Nat st i in Seg n holds
D . i is Interval ) & I = CarProduct D implies ( [:I,J:] is Subset of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:] & [:I,J:] in sigma (measurable_rectangles ((Prod_Field (L-Field n)),L-Field)) ) )
assume that
A1: for i being Nat st i in Seg n holds
D . i is Interval and
A2: I = CarProduct D ; :: thesis: ( [:I,J:] is Subset of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:] & [:I,J:] in sigma (measurable_rectangles ((Prod_Field (L-Field n)),L-Field)) )
I is Element of Prod_Field (L-Field n) by A1, A2, Th9;
then ( I in Prod_Field (L-Field n) & J in L-Field ) by MEASUR10:5, MEASUR12:75;
then A3: [:I,J:] in measurable_rectangles ((Prod_Field (L-Field n)),L-Field) ;
reconsider J1 = J as Subset of RNS_Real ;
A4: [:I,J:] = [:I,J1:] ;
measurable_rectangles ((Prod_Field (L-Field n)),L-Field) c= sigma (measurable_rectangles ((Prod_Field (L-Field n)),L-Field)) by PROB_1:def 9;
hence ( [:I,J:] is Subset of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:] & [:I,J:] in sigma (measurable_rectangles ((Prod_Field (L-Field n)),L-Field)) ) by A3, A4; :: thesis: verum