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 f being n -element FinSequence of [:REAL,REAL:] st
( x = y & ( 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).] ) ) )
let x be object ; :: thesis: ( x in MeasurableRectangle (ProductLeftOpenIntervals n) implies ex y being Subset of (REAL n) ex f being n -element FinSequence of [:REAL,REAL:] st
( x = y & ( 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).] ) ) ) )
assume A1: x in MeasurableRectangle (ProductLeftOpenIntervals n) ; :: thesis: ex y being Subset of (REAL n) ex f being n -element FinSequence of [:REAL,REAL:] st
( x = y & ( 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).] ) ) )
MeasurableRectangle (ProductLeftOpenIntervals n) is Subset-Family of (REAL n) by Th30;
then reconsider y = x as Subset of (REAL n) by A1;
take y ; :: thesis: ex f being n -element FinSequence of [:REAL,REAL:] st
( x = y & ( 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).] ) ) )
reconsider x0 = x as set by TARSKI:1;
consider g being Function such that
A2: x = product g and
A3: g in product (ProductLeftOpenIntervals n) by A1, SRINGS_4:def 4;
dom (ProductLeftOpenIntervals n) = Seg n by FUNCOP_1:13;
then A4: dom g = Seg n by A3, CARD_3:9;
A5: now :: thesis: for i being Nat st i in Seg n holds
ex a, b being Real st g . i = ].a,b.]
let i be Nat; :: thesis: ( i in Seg n implies ex a, b being Real st g . i = ].a,b.] )
assume A6: i in Seg n ; :: thesis: ex a, b being Real st g . i = ].a,b.]
then i in dom (ProductLeftOpenIntervals n) by FUNCOP_1:13;
then g . i in (ProductLeftOpenIntervals n) . i by A3, CARD_3:9;
then g . i in the_set_of_all_left_open_real_bounded_intervals by A6, FUNCOP_1:7;
hence ex a, b being Real st g . i = ].a,b.] ; :: thesis: verum
end;
defpred S1[ Nat, set ] means ex x being Element of [:REAL,REAL:] st
( $2 = x & g . $1 = ].(x `1),(x `2).] );
A7: for i being Nat st i in Seg n holds
ex d being Element of [:REAL,REAL:] st S1[i,d]
proof
let i be Nat; :: thesis: ( i in Seg n implies ex d being Element of [:REAL,REAL:] st S1[i,d] )
assume i in Seg n ; :: thesis: ex d being Element of [:REAL,REAL:] st S1[i,d]
then consider a, b being Real such that
A8: g . i = ].a,b.] by A5;
set d = [a,b];
( a in REAL & b in REAL ) by XREAL_0:def 1;
then reconsider d = [a,b] as Element of [:REAL,REAL:] by ZFMISC_1:def 2;
take d ; :: thesis: S1[i,d]
( d is Element of [:REAL,REAL:] & g . i = ].(d `1),(d `2).] ) by A8;
hence S1[i,d] ; :: thesis: verum
end;
ex f2 being FinSequence of [:REAL,REAL:] st
( len f2 = n & ( for i being Nat st i in Seg n holds
S1[i,f2 /. i] ) ) from FINSEQ_4:sch 1(A7);
 then consider f2 being FinSequence of [:REAL,REAL:] such that
A9: len f2 = n and
A10: for i being Nat st i in Seg n holds
ex x being Element of [:REAL,REAL:] st
( f2 /. i = x & g . i = ].(x `1),(x `2).] ) ;
reconsider f2 = f2 as n -element FinSequence of [:REAL,REAL:] by A9, CARD_1:def 7;
take f2 ; :: thesis: ( x = y & ( 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 ].((f2 /. i) `1),((f2 /. i) `2).] ) ) )
thus x = y ; :: thesis: 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 ].((f2 /. i) `1),((f2 /. i) `2).] )
A11: for i being Nat st i in Seg n holds
g . i = ].((f2 /. i) `1),((f2 /. i) `2).]
proof
let i be Nat; :: thesis: ( i in Seg n implies g . i = ].((f2 /. i) `1),((f2 /. i) `2).] )
assume i in Seg n ; :: thesis: g . i = ].((f2 /. i) `1),((f2 /. i) `2).]
then consider x being Element of [:REAL,REAL:] such that
A12: f2 /. i = x and
A13: g . i = ].(x `1),(x `2).] by A10;
thus g . i = ].((f2 /. i) `1),((f2 /. i) `2).] by A12, A13; :: thesis: verum
end;
A14: for t being Element of REAL n st t in y holds
for i being Nat st i in Seg n holds
t . i in ].((f2 /. i) `1),((f2 /. i) `2).]
proof
let t be Element of REAL n; :: thesis: ( t in y implies for i being Nat st i in Seg n holds
t . i in ].((f2 /. i) `1),((f2 /. i) `2).] )
assume t in y ; :: thesis: for i being Nat st i in Seg n holds
t . i in ].((f2 /. i) `1),((f2 /. i) `2).]
then consider j0 being Function such that
A15: t = j0 and
dom j0 = Seg n and
A16: for y being object st y in Seg n holds
j0 . y in g . y by A2, CARD_3:def 5, A4;
now :: thesis: for i being Nat st i in Seg n holds
t . i in ].((f2 /. i) `1),((f2 /. i) `2).]
let i be Nat; :: thesis: ( i in Seg n implies t . i in ].((f2 /. i) `1),((f2 /. i) `2).] )
assume A17: i in Seg n ; :: thesis: t . i in ].((f2 /. i) `1),((f2 /. i) `2).]
then t . i in g . i by A15, A16;
hence t . i in ].((f2 /. i) `1),((f2 /. i) `2).] by A17, A11; :: thesis: verum
end;
hence for i being Nat st i in Seg n holds
t . i in ].((f2 /. i) `1),((f2 /. i) `2).] ; :: thesis: verum
end;
for t being Element of REAL n st ( for i being Nat st i in Seg n holds
t . i in ].((f2 /. i) `1),((f2 /. i) `2).] ) holds
t in y
proof
let t be Element of REAL n; :: thesis: ( ( for i being Nat st i in Seg n holds
t . i in ].((f2 /. i) `1),((f2 /. i) `2).] ) implies t in y )
assume A18: for i being Nat st i in Seg n holds
t . i in ].((f2 /. i) `1),((f2 /. i) `2).] ; :: thesis: t in y
reconsider j = t as Function ;
t is Element of Funcs ((Seg n),REAL) by FINSEQ_2:93;
then A19: ex j0 being Function st
( j = j0 & dom j0 = Seg n & rng j0 c= REAL ) by FUNCT_2:def 2;
for y being object st y in Seg n holds
j . y in g . y
proof
let y be object ; :: thesis: ( y in Seg n implies j . y in g . y )
assume A20: y in Seg n ; :: thesis: j . y in g . y
then reconsider y1 = y as Nat ;
g . y1 = ].((f2 /. y1) `1),((f2 /. y1) `2).] by A20, A11;
hence j . y in g . y by A20, A18; :: thesis: verum
end;
hence t in y by A19, A2, CARD_3:def 5, A4; :: thesis: verum
end;
hence 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 ].((f2 /. i) `1),((f2 /. i) `2).] ) by A14; :: thesis: verum