let n be non zero Nat; :: thesis: for x being object st x in MeasurableRectangle (ProductRightOpenIntervals 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 (ProductRightOpenIntervals 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 (ProductRightOpenIntervals 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 (ProductRightOpenIntervals n) is Subset-Family of (REAL n) by Th33;
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 (ProductRightOpenIntervals n) by A1, SRINGS_4:def 4;
dom (ProductRightOpenIntervals 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 (ProductRightOpenIntervals n) by FUNCOP_1:13;
then g . i in (ProductRightOpenIntervals 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