let n be non zero Nat; for x being object st x in MeasurableRectangle (ProductLeftOpenIntervals n) holds
ex y being Subset of (REAL n) ex a, b being Element of REAL n st
( x = y & ( for s being object holds
( s in y iff ex t being Element of REAL n st
( s = t & ( for i being Nat st i in Seg n holds
t . i in ].(a . i),(b . i).] ) ) ) ) )
let x be object ; ( x in MeasurableRectangle (ProductLeftOpenIntervals n) implies ex y being Subset of (REAL n) ex a, b being Element of REAL n st
( x = y & ( for s being object holds
( s in y iff ex t being Element of REAL n st
( s = t & ( for i being Nat st i in Seg n holds
t . i in ].(a . i),(b . i).] ) ) ) ) ) )
assume
x in MeasurableRectangle (ProductLeftOpenIntervals n)
; ex y being Subset of (REAL n) ex a, b being Element of REAL n st
( x = y & ( for s being object holds
( s in y iff ex t being Element of REAL n st
( s = t & ( 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 Th31;
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
y
; ex a, b being Element of REAL n st
( x = y & ( for s being object holds
( s in y iff ex t being Element of REAL n st
( s = t & ( for i being Nat st i in Seg n holds
t . i in ].(a . i),(b . i).] ) ) ) ) )
take
y1
; ex b being Element of REAL n st
( x = y & ( for s being object holds
( s in y iff ex t being Element of REAL n st
( s = t & ( for i being Nat st i in Seg n holds
t . i in ].(y1 . i),(b . i).] ) ) ) ) )
take
z1
; ( x = y & ( for s being object holds
( s in y iff ex t being Element of REAL n st
( s = t & ( for i being Nat st i in Seg n holds
t . i in ].(y1 . i),(z1 . i).] ) ) ) ) )
thus
x = y
by A1; for s being object holds
( s in y iff ex t being Element of REAL n st
( s = t & ( for i being Nat st i in Seg n holds
t . i in ].(y1 . i),(z1 . i).] ) ) )
thus
for s being object holds
( s in y iff ex t being Element of REAL n st
( s = t & ( for i being Nat st i in Seg n holds
t . i in ].(y1 . i),(z1 . i).] ) ) )
verum