let n be non zero Nat; :: thesis: for x being Subset of (REAL n)
for 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).[ ) ) holds
x is Element of Product (n,the_set_of_all_right_open_real_bounded_intervals)
let x be Subset of (REAL n); :: thesis: for 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).[ ) ) holds
x is Element of Product (n,the_set_of_all_right_open_real_bounded_intervals)
let a, b be Element of REAL n; :: 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 [.(a . i),(b . i).[ ) ) implies x is Element of Product (n,the_set_of_all_right_open_real_bounded_intervals) )
assume A1: 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).[ ) ; :: thesis: x is Element of Product (n,the_set_of_all_right_open_real_bounded_intervals)
defpred S₁[ object , object ] means ex n being Nat st
( $1 = n & $2 = [.(a . n),(b . n).[ );
A2: for i being Nat st i in Seg n holds
ex d being Element of the_set_of_all_right_open_real_bounded_intervals st S₁[i,d]

proof

let i be Nat; :: thesis: ( i in Seg n implies ex d being Element of the_set_of_all_right_open_real_bounded_intervals st S₁[i,d] )
assume i in Seg n ; :: thesis: ex d being Element of the_set_of_all_right_open_real_bounded_intervals st S₁[i,d]
set d = [.(a . i),(b . i).[;
take [.(a . i),(b . i).[ ; :: thesis: ( [.(a . i),(b . i).[ is Element of the_set_of_all_right_open_real_bounded_intervals & S₁[i,[.(a . i),(b . i).[] )
[.(a . i),(b . i).[ in { [.a,b.[ where a, b is Real : verum } ;
hence [.(a . i),(b . i).[ is Element of the_set_of_all_right_open_real_bounded_intervals ; :: thesis: S₁[i,[.(a . i),(b . i).[]
thus S₁[i,[.(a . i),(b . i).[] ; :: thesis: verum

end;

ex g being FinSequence of the_set_of_all_right_open_real_bounded_intervals st
( len g = n & ( for i being Nat st i in Seg n holds
S₁[i,g /. i] ) ) from FINSEQ_4:sch 1(A2);
then consider g being FinSequence of the_set_of_all_right_open_real_bounded_intervals such that
A3: len g = n and
A4: for i being Nat st i in Seg n holds
S₁[i,g /. i] ;
A5: for i being Nat st i in Seg n holds
g . i = [.(a . i),(b . i).[

proof

let i be Nat; :: thesis: ( i in Seg n implies g . i = [.(a . i),(b . i).[ )
assume A6: i in Seg n ; :: thesis: g . i = [.(a . i),(b . i).[
then S₁[i,g /. i] by A4;
then consider m being object such that
A7: m = i and
A8: g /. m = [.(a . m),(b . m).[ ;
i in dom g by A6, A3, FINSEQ_1:def 3;
hence g . i = [.(a . i),(b . i).[ by A7, A8, PARTFUN1:def 6; :: thesis: verum

end;

ex g being Function st
( x = product g & g in product ((Seg n) --> the_set_of_all_right_open_real_bounded_intervals) )

proof

take g ; :: thesis: ( x = product g & g in product ((Seg n) --> the_set_of_all_right_open_real_bounded_intervals) )
thus x = product g :: thesis: g in product ((Seg n) --> the_set_of_all_right_open_real_bounded_intervals)

proof

for t being object holds
( t in x iff ex h being Function st
( t = h & dom h = dom g & ( for u being object st u in dom g holds
h . u in g . u ) ) )

proof

let t be object ; :: thesis: ( t in x iff ex h being Function st
( t = h & dom h = dom g & ( for u being object st u in dom g holds
h . u in g . u ) ) )

hereby :: thesis: ( ex h being Function st
( t = h & dom h = dom g & ( for u being object st u in dom g holds
h . u in g . u ) ) implies t in x )

assume A9: t in x ; :: thesis: ex h being Function st
( t = h & dom h = dom g & ( for u being object st u in dom g holds
h . u in g . u ) )
then reconsider t1 = t as Element of REAL n ;
A10: dom t1 = Seg n by FINSEQ_1:89;

now :: thesis: ( dom t1 = dom g & ( for u being object st u in dom g holds
t1 . u in g . u ) )

thus dom t1 = dom g by A10, A3, FINSEQ_1:def 3; :: thesis: for u being object st u in dom g holds
t1 . u in g . u
thus for u being object st u in dom g holds
t1 . u in g . u :: thesis: verum

proof

let u be object ; :: thesis: ( u in dom g implies t1 . u in g . u )
assume u in dom g ; :: thesis: t1 . u in g . u
then A11: u in Seg n by A3, FINSEQ_1:def 3;
then t1 . u in [.(a . u),(b . u).[ by A9, A1;
hence t1 . u in g . u by A11, A5; :: thesis: verum

end;

end;

hence ex h being Function st
( t = h & dom h = dom g & ( for u being object st u in dom g holds
h . u in g . u ) ) ; :: thesis: verum

end;

hereby :: thesis: verum

given h being Function such that A12: t = h and
A13: dom h = dom g and
A14: for u being object st u in dom g holds
h . u in g . u ; :: thesis: t in x
A15: for i being Nat st i in Seg n holds
h . i in [.(a . i),(b . i).[

proof

let i be Nat; :: thesis: ( i in Seg n implies h . i in [.(a . i),(b . i).[ )
assume A16: i in Seg n ; :: thesis: h . i in [.(a . i),(b . i).[
then i in dom g by A3, FINSEQ_1:def 3;
then h . i in g . i by A14;
hence h . i in [.(a . i),(b . i).[ by A16, A5; :: thesis: verum

end;

( dom h = dom ((Seg n) --> REAL) & ( for u being object st u in dom ((Seg n) --> REAL) holds
h . u in ((Seg n) --> REAL) . u ) )

proof

dom h = Seg n by A13, A3, FINSEQ_1:def 3;
hence dom h = dom ((Seg n) --> REAL) by FUNCOP_1:13; :: thesis: for u being object st u in dom ((Seg n) --> REAL) holds
h . u in ((Seg n) --> REAL) . u

hereby :: thesis: verum

let u be object ; :: thesis: ( u in dom ((Seg n) --> REAL) implies h . u in ((Seg n) --> REAL) . u )
assume A17: u in dom ((Seg n) --> REAL) ; :: thesis: h . u in ((Seg n) --> REAL) . u
then A18: u in Seg n ;
( h . u in [.(a . u),(b . u).[ & [.(a . u),(b . u).[ c= REAL ) by A17, A15;
then ( h . u in REAL & u in dom g ) by A18, A3, FINSEQ_1:def 3;
hence h . u in ((Seg n) --> REAL) . u by FUNCOP_1:7, A17; :: thesis: verum

end;

end;

then h in product ((Seg n) --> REAL) by CARD_3:9;
then reconsider h = h as Element of REAL n by Th7;
h in x by A15, A1;
hence t in x by A12; :: thesis: verum

end;

end;

hence x = product g by CARD_3:def 5; :: thesis: verum

end;

thus g in product ((Seg n) --> the_set_of_all_right_open_real_bounded_intervals) :: thesis: verum

proof

A19: ( dom g = Seg n & dom ((Seg n) --> the_set_of_all_right_open_real_bounded_intervals) = Seg n ) by A3, FINSEQ_1:def 3, FUNCOP_1:13;
for x being object st x in dom ((Seg n) --> the_set_of_all_right_open_real_bounded_intervals) holds
g . x in ((Seg n) --> the_set_of_all_right_open_real_bounded_intervals) . x

proof

let x be object ; :: thesis: ( x in dom ((Seg n) --> the_set_of_all_right_open_real_bounded_intervals) implies g . x in ((Seg n) --> the_set_of_all_right_open_real_bounded_intervals) . x )
assume A20: x in dom ((Seg n) --> the_set_of_all_right_open_real_bounded_intervals) ; :: thesis: g . x in ((Seg n) --> the_set_of_all_right_open_real_bounded_intervals) . x
then g . x = [.(a . x),(b . x).[ by A5;
then ( g . x in the_set_of_all_right_open_real_bounded_intervals & ((Seg n) --> the_set_of_all_right_open_real_bounded_intervals) . x = the_set_of_all_right_open_real_bounded_intervals ) by A20, FUNCOP_1:7;
hence g . x in ((Seg n) --> the_set_of_all_right_open_real_bounded_intervals) . x ; :: thesis: verum

end;

hence g in product ((Seg n) --> the_set_of_all_right_open_real_bounded_intervals) by A19, CARD_3:9; :: thesis: verum

end;

end;

hence x is Element of Product (n,the_set_of_all_right_open_real_bounded_intervals) by Def2; :: thesis: verum