let n be non zero Nat; :: thesis:
let x be Subset of (REAL n); :: thesis:
let a, b be Element of REAL n; :: thesis:
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:
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_left_open_real_bounded_intervals st S₁[i,d]

let i be Nat; :: thesis:
assume i in Seg n ; :: thesis:
set d = ].(a . i),(b . i).];
take ].(a . i),(b . i).] ; :: thesis:
].(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_left_open_real_bounded_intervals ; :: thesis:
thus S₁[i,].(a . i),(b . i).]] ; :: thesis:

end;

ex g being FinSequence of the_set_of_all_left_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_left_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).]

let i be Nat; :: thesis:
assume A6: i in Seg n ; :: thesis:
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:

end;

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

take g ; :: thesis:
thus x = product g :: thesis:

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 ) ) )

let t be object ; :: thesis:

hereby :: thesis:

assume A9: t in x ; :: thesis:
then reconsider t1 = t as Element of REAL n ;
A10: dom t1 = Seg n by FINSEQ_1:89;

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

let u be object ; :: thesis:
assume u in dom g ; :: thesis:
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:

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:

end;

hereby :: thesis:

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:
A15: for i being Nat st i in Seg n holds
h . i in ].(a . i),(b . i).]

let i be Nat; :: thesis:
assume A16: i in Seg n ; :: thesis:
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:

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 ) )

dom h = Seg n by A13, A3, FINSEQ_1:def 3;
hence dom h = dom ((Seg n) --> REAL) by FUNCOP_1:13; :: thesis:

hereby :: thesis:

let u be object ; :: thesis:
assume A17: u in dom ((Seg n) --> REAL) ; :: thesis:
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:

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:

end;

end;

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

end;

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

A19: ( dom g = Seg n & dom ((Seg n) --> the_set_of_all_left_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_left_open_real_bounded_intervals) holds
g . x in ((Seg n) --> the_set_of_all_left_open_real_bounded_intervals) . x

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

end;

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

end;

end;

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