let n be non zero Nat; :: thesis: for x being object st x in MeasurableRectangle (ProductLeftOpenIntervals n) holds
ex y being Subset of (REAL n) st
( x = y & ( for i being Nat st i in Seg n holds
ex a, b being Real st
for t being Element of REAL n st t in y holds
t . i in ].a,b.] ) )
let x be object ; :: thesis: ( x in MeasurableRectangle (ProductLeftOpenIntervals n) implies ex y being Subset of (REAL n) st
( x = y & ( for i being Nat st i in Seg n holds
ex a, b being Real st
for t being Element of REAL n st t in y holds
t . i in ].a,b.] ) ) )
assume A1: x in MeasurableRectangle (ProductLeftOpenIntervals n) ; :: thesis: ex y being Subset of (REAL n) st
( x = y & ( for i being Nat st i in Seg n holds
ex a, b being Real st
for t being Element of REAL n st t in y holds
t . i in ].a,b.] ) )
MeasurableRectangle (ProductLeftOpenIntervals n) is Subset-Family of (REAL n) by Th30;
then reconsider y = x as Subset of (REAL n) by A1;
reconsider x0 = x as set by TARSKI:1;
consider g being Function such that
A2: x = product g and
A3: g in product (ProductLeftOpenIntervals n) by A1, SRINGS_4:def 4;
dom (ProductLeftOpenIntervals n) = Seg n by FUNCOP_1:13;
then A4: dom g = Seg n by A3, CARD_3:9;
take y ; :: thesis: ( x = y & ( for i being Nat st i in Seg n holds
ex a, b being Real st
for t being Element of REAL n st t in y holds
t . i in ].a,b.] ) )
thus x = y ; :: thesis: for i being Nat st i in Seg n holds
ex a, b being Real st
for t being Element of REAL n st t in y holds
t . i in ].a,b.]
now :: thesis: for i being Nat st i in Seg n holds
( ex a, b, a, b being Real st
for t being Element of REAL n st t in y holds
t . i in ].a,b.] & ex a, b being Real st
for t being Element of REAL n st t in y holds
t . i in ].a,b.] )
let i be Nat; :: thesis: ( i in Seg n implies ( ex a, b, a, b being Real st
for t being Element of REAL n st t in y holds
t . i in ].a,b.] & ex a, b being Real st
for t being Element of REAL n st t in y holds
t . i in ].a,b.] ) )
assume A5: i in Seg n ; :: thesis: ( ex a, b, a, b being Real st
for t being Element of REAL n st t in y holds
t . i in ].a,b.] & ex a, b being Real st
for t being Element of REAL n st t in y holds
t . i in ].a,b.] )
then i in dom (ProductLeftOpenIntervals n) by FUNCOP_1:13;
then g . i in (ProductLeftOpenIntervals n) . i by A3, CARD_3:9;
then g . i in { ].a,b.] where a, b is Real : verum } by A5, FUNCOP_1:7;
then consider a, b being Real such that
A6: g . i = ].a,b.] ;
hereby :: thesis: ex a, b being Real st
for t being Element of REAL n st t in y holds
t . i in ].a,b.]
take a = a; :: thesis: ex b, a, b being Real st
for t being Element of REAL n st t in y holds
t . i in ].a,b.]
take b = b; :: thesis: ex a, b being Real st
for t being Element of REAL n st t in y holds
t . i in ].a,b.]
now :: thesis: for t being Element of REAL n st t in y holds
t . i in ].a,b.]
let t be Element of REAL n; :: thesis: ( t in y implies t . i in ].a,b.] )
assume t in y ; :: thesis: t . i in ].a,b.]
then consider j0 being Function such that
A7: t = j0 and
dom j0 = Seg n and
A8: for u being object st u in Seg n holds
j0 . u in g . u by A2, CARD_3:def 5, A4;
thus t . i in ].a,b.] by A7, A6, A8, A5; :: thesis: verum
end;
hence ex a, b being Real st
for t being Element of REAL n st t in y holds
t . i in ].a,b.] ; :: thesis: verum
end;
hence ex a, b being Real st
for t being Element of REAL n st t in y holds
t . i in ].a,b.] ; :: thesis: verum
end;
hence for i being Nat st i in Seg n holds
ex a, b being Real st
for t being Element of REAL n st t in y holds
t . i in ].a,b.] ; :: thesis: verum