let n be non zero Nat; :: thesis: 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 ; :: thesis: ( 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) ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: 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).[ )
proof
A7: now :: thesis: for t being Element of REAL n st t in x holds
for i being Nat st i in Seg n holds
t . i in [.(y1 . i),(z1 . i).[
let t be Element of REAL n; :: thesis: ( t in x implies for i being Nat st i in Seg n holds
t . i in [.(y1 . i),(z1 . i).[ )
assume A8: t in x ; :: 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, A1, A2; :: thesis: verum
end;
end;
now :: thesis: for t being Element of REAL n st ( for i being Nat st i in Seg n holds
t . i in [.(y1 . i),(z1 . i).[ ) holds
t in x
let t be Element of REAL n; :: thesis: ( ( for i being Nat st i in Seg n holds
t . i in [.(y1 . i),(z1 . i).[ ) implies t in x )
assume A10: for i being Nat st i in Seg n holds
t . i in [.(y1 . i),(z1 . i).[ ; :: thesis: t in x
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 A11: 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 A10, A11, A6; :: thesis: verum
end;
hence t in x by A1, A2; :: thesis: verum
end;
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).[ ) by A7; :: thesis: verum
end;
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).[ ) ; :: thesis: verum