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) 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 ; :: thesis: ( 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) ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: 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).] ) ) ) :: thesis: verum

proof

let s be object ; :: thesis: ( 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).] ) ) )

hereby :: thesis: ( 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).] ) ) implies s in y )

assume A8: s in y ; :: thesis: 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).] ) )
then reconsider t = s as Element of REAL n ;

now :: thesis: 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).] ) )

take t = t; :: thesis: ( s = t & ( for i being Nat st i in Seg n holds
t . i in ].(y1 . i),(z1 . i).] ) )
thus s = t ; :: thesis: for i being Nat st i in Seg n holds
t . i in ].(y1 . i),(z1 . i).]

hereby :: thesis: verum

let i be Nat; :: thesis: ( i in Seg n implies t . i in ].(y1 . i),(z1 . i).] )
assume A9: i in Seg n ; :: thesis: t . i in ].(y1 . i),(z1 . i).]
then ( (x1 `1) . i = (f /. i) `1 & (x1 `2) . i = (f /. i) `2 ) by A3;
hence t . i in ].(y1 . i),(z1 . i).] by A6, A8, A9, A2; :: thesis: verum

end;

end;

hence 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).] ) ) ; :: thesis: verum

end;

assume 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).] ) ) ; :: thesis: s in y
then consider t being Element of REAL n such that
A10: s = t and
A11: for i being Nat st i in Seg n holds
t . i in ].(y1 . i),(z1 . i).] ;

now :: thesis: for i being Nat st i in Seg n holds
t . i in ].((f /. i) `1),((f /. i) `2).]

let i be Nat; :: thesis: ( i in Seg n implies t . i in ].((f /. i) `1),((f /. i) `2).] )
assume A12: i in Seg n ; :: thesis: t . i in ].((f /. i) `1),((f /. i) `2).]
then ( (x1 `1) . i = (f /. i) `1 & (x1 `2) . i = (f /. i) `2 ) by A3;
hence t . i in ].((f /. i) `1),((f /. i) `2).] by A11, A12, A6; :: thesis: verum

end;

hence s in y by A10, A2; :: thesis: verum

end;