let n be non zero Nat; :: thesis: for s being Tuple of n, the_set_of_all_right_open_real_bounded_intervals ex a, b being Element of REAL n st
for i being Nat st i in Seg n holds
s . i = [.(a . i),(b . i).[
let s be Tuple of n, the_set_of_all_right_open_real_bounded_intervals ; :: thesis: ex a, b being Element of REAL n st
for i being Nat st i in Seg n holds
s . i = [.(a . i),(b . i).[
s in Funcs ((Seg n),the_set_of_all_right_open_real_bounded_intervals) by Th9;
then consider f being Function such that
A1: s = f and
A2: dom f = Seg n and
rng f c= the_set_of_all_right_open_real_bounded_intervals by FUNCT_2:def 2;
defpred S₁[ object , object ] means ex f being Element of [:REAL,REAL:] st
( f = $2 & s . $1 = [.(f `1),(f `2).[ );
A3: for i being Nat st i in Seg n holds
ex d being Element of [:REAL,REAL:] st S₁[i,d]

proof

let i be Nat; :: thesis: ( i in Seg n implies ex d being Element of [:REAL,REAL:] st S₁[i,d] )
assume i in Seg n ; :: thesis: ex d being Element of [:REAL,REAL:] st S₁[i,d]
then s . i in rng s by A1, A2, FUNCT_1:3;
then s . i in { [.a,b.[ where a, b is Real : verum } ;
then consider a, b being Real such that
A4: s . i = [.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: S₁[i,d]
s . i = [.(d `1),(d `2).[ by A4;
hence S₁[i,d] ; :: thesis: verum

end;

consider f being FinSequence of [:REAL,REAL:] such that
A5: len f = n and
A6: for i being Nat st i in Seg n holds
S₁[i,f /. i] from FINSEQ_4:sch 1(A3);
reconsider f = f as n -element FinSequence of [:REAL,REAL:] by A5, CARD_1:def 7;
consider z being Element of [:(REAL n),(REAL n):] such that
A7: for i being Nat st i in Seg n holds
( (z `1) . i = (f /. i) `1 & (z `2) . i = (f /. i) `2 ) by Th13;
reconsider a = z `1 , b = z `2 as Element of REAL n ;
take a ; :: thesis: ex b being Element of REAL n st
for i being Nat st i in Seg n holds
s . i = [.(a . i),(b . i).[
take b ; :: thesis: for i being Nat st i in Seg n holds
s . i = [.(a . i),(b . i).[
thus for i being Nat st i in Seg n holds
s . i = [.(a . i),(b . i).[ :: thesis: verum

proof

let i be Nat; :: thesis: ( i in Seg n implies s . i = [.(a . i),(b . i).[ )
assume i in Seg n ; :: thesis: s . i = [.(a . i),(b . i).[
then ( a . i = (f /. i) `1 & b . i = (f /. i) `2 & S₁[i,f /. i] ) by A6, A7;
hence s . i = [.(a . i),(b . i).[ ; :: thesis: verum

end;