let n be non zero Nat; for x being set st x in MeasurableRectangle (ProductRightOpenIntervals n) holds
ex a, b being Element of REAL n st
for t being Element of REAL n holds
( t in x iff for i being Nat st i in Seg n holds
t . i in [.(a . i),(b . i).[ )
let x be set ; ( x in MeasurableRectangle (ProductRightOpenIntervals n) implies ex a, b being Element of REAL n st
for t being Element of REAL n holds
( t in x iff for i being Nat st i in Seg n holds
t . i in [.(a . i),(b . i).[ ) )
assume
x in MeasurableRectangle (ProductRightOpenIntervals n)
; ex a, b being Element of REAL n st
for t being Element of REAL n holds
( t in x iff for i being Nat st i in Seg n holds
t . i in [.(a . i),(b . i).[ )
then consider y being Subset of (REAL n), f being n -element FinSequence of [:REAL,REAL:] such that
A1:
x = y
and
A2:
for t being Element of REAL n holds
( t in y iff for i being Nat st i in Seg n holds
t . i in [.((f /. i) `1),((f /. i) `2).[ )
by Th34;
consider x1 being Element of [:(REAL n),(REAL n):] such that
A3:
for i being Nat st i in Seg n holds
( (x1 `1) . i = (f /. i) `1 & (x1 `2) . i = (f /. i) `2 )
by Th13;
consider y1, z1 being object such that
A4:
y1 in REAL n
and
A5:
z1 in REAL n
and
A6:
x1 = [y1,z1]
by ZFMISC_1:def 2;
reconsider y1 = y1, z1 = z1 as Element of REAL n by A4, A5;
take
y1
; ex b being Element of REAL n st
for t being Element of REAL n holds
( t in x iff for i being Nat st i in Seg n holds
t . i in [.(y1 . i),(b . i).[ )
take
z1
; for t being Element of REAL n holds
( t in x iff for i being Nat st i in Seg n holds
t . i in [.(y1 . i),(z1 . i).[ )
for t being Element of REAL n holds
( t in x iff for i being Nat st i in Seg n holds
t . i in [.(y1 . i),(z1 . i).[ )
hence
for t being Element of REAL n holds
( t in x iff for i being Nat st i in Seg n holds
t . i in [.(y1 . i),(z1 . i).[ )
; verum